Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mp3an2 | Structured version Visualization version Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an2.1 | |
mp3an2.2 |
Ref | Expression |
---|---|
mp3an2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an2.1 | . 2 | |
2 | mp3an2.2 | . . 3 | |
3 | 2 | 3expa 1265 | . 2 |
4 | 1, 3 | mpanl2 717 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 386 df-3an 1039 |
This theorem is referenced by: mp3anl2 1419 tz7.7 5749 ordin 5753 onfr 5763 wfrlem14 7428 wfrlem17 7431 tfrlem11 7484 epfrs 8607 zorng 9326 tsk2 9587 tskcard 9603 gruina 9640 muladd11 10206 00id 10211 ltaddneg 10251 negsub 10329 subneg 10330 muleqadd 10671 diveq1 10718 conjmul 10742 recp1lt1 10921 nnsub 11059 addltmul 11268 nnunb 11288 zltp1le 11427 gtndiv 11454 eluzp1m1 11711 zbtwnre 11786 rebtwnz 11787 xnn0le2is012 12076 supxrbnd 12158 divelunit 12314 fznatpl1 12395 flbi2 12618 fldiv 12659 modid 12695 modm1p1mod0 12721 fzen2 12768 nn0ennn 12778 seqshft2 12827 seqf1olem1 12840 ser1const 12857 sq01 12986 expnbnd 12993 faclbnd3 13079 faclbnd5 13085 hashunsng 13181 hashxplem 13220 ccatrid 13370 sgnn 13834 sqrlem2 13984 sqrlem7 13989 leabs 14039 abs2dif 14072 cvgrat 14615 cos2t 14908 sin01gt0 14920 cos01gt0 14921 demoivre 14930 demoivreALT 14931 znnenlem 14940 rpnnen2lem5 14947 rpnnen2lem12 14954 omeo 15090 gcd0id 15240 sqgcd 15278 isprm3 15396 eulerthlem2 15487 pczpre 15552 pcrec 15563 ressress 15938 mulgm1 17562 unitgrpid 18669 mdet0pr 20398 m2detleib 20437 cmpcov2 21193 ufileu 21723 tgpconncompeqg 21915 itg2ge0 23502 mdegldg 23826 abssinper 24270 ppiub 24929 chtub 24937 bposlem2 25010 lgs1 25066 colinearalglem4 25789 axsegconlem1 25797 axpaschlem 25820 axcontlem2 25845 axcontlem4 25847 axcontlem7 25850 axcontlem8 25851 funvtxval 25905 funiedgval 25906 vc0 27429 vcm 27431 nvmval2 27498 nvmf 27500 nvmdi 27503 nvnegneg 27504 nvpncan2 27508 nvaddsub4 27512 nvm1 27520 nvdif 27521 nvpi 27522 nvz0 27523 nvmtri 27526 nvabs 27527 nvge0 27528 imsmetlem 27545 4ipval2 27563 ipval3 27564 ipidsq 27565 dipcj 27569 sspmval 27588 ipasslem1 27686 ipasslem2 27687 dipsubdir 27703 hvsubdistr1 27906 shsubcl 28077 shsel3 28174 shunssi 28227 hosubdi 28667 lnopmi 28859 nmophmi 28890 nmopcoi 28954 opsqrlem6 29004 hstle 29089 hst0 29092 mdsl2i 29181 superpos 29213 dmdbr5ati 29281 resvsca 29830 cvmliftphtlem 31299 topdifinffinlem 33195 finixpnum 33394 tan2h 33401 poimirlem3 33412 poimirlem4 33413 poimirlem7 33416 poimirlem16 33425 poimirlem17 33426 poimirlem19 33428 poimirlem20 33429 poimirlem24 33433 poimirlem28 33437 mblfinlem2 33447 mblfinlem4 33449 ismblfin 33450 el3v2 33989 atlatle 34607 pmaple 35047 dihglblem2N 36583 elnnrabdioph 37371 rabren3dioph 37379 zindbi 37511 expgrowth 38534 binomcxplemnotnn0 38555 trelpss 38659 etransc 40500 mogoldbb 41673 pgrple2abl 42146 aacllem 42547 |
Copyright terms: Public domain | W3C validator |