![]() |
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 1208 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpanl2 687 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 189 df-an 373 df-3an 987 |
This theorem is referenced by: mp3anl2 1359 tz7.7 5449 ordin 5453 onfr 5462 wfrlem14 7049 wfrlem17 7052 tfrlem11 7106 epfrs 8215 zorng 8934 tsk2 9190 tskcard 9206 gruina 9243 muladd11 9803 00id 9808 negsub 9922 subneg 9923 muleqadd 10256 diveq1 10301 conjmul 10324 recp1lt1 10504 nnsub 10648 addltmul 10848 nnunb 10865 zltp1le 10986 gtndiv 11013 eluzp1m1 11182 zbtwnre 11262 rebtwnz 11263 supxrbnd 11614 divelunit 11774 fznatpl1 11850 flbi2 12052 fldiv 12087 modid 12121 modm1p1mod0 12141 fzen2 12182 nn0ennn 12192 seqshft2 12239 seqf1olem1 12252 ser1const 12269 sq01 12394 expnbnd 12401 faclbnd3 12477 faclbnd5 12483 hashunsng 12571 hashxplem 12605 ccatrid 12731 sgnn 13157 sqrlem2 13307 sqrlem7 13312 leabs 13362 abs2dif 13395 cvgrat 13939 cos2t 14232 sin01gt0 14244 cos01gt0 14245 demoivre 14254 demoivreALT 14255 znnenlem 14264 rpnnen2lem5 14271 rpnnen2 14278 gcd0id 14487 sqgcd 14526 isprm3 14633 eulerthlem2 14730 omeo 14764 pczpre 14797 pcrec 14808 ressress 15187 mulgm1 16777 unitgrpid 17897 mdet0pr 19617 m2detleib 19656 cmpcov2 20405 ufileu 20934 tgpconcompeqg 21126 itg2ge0 22693 mdegldg 23015 abssinper 23473 ppiub 24132 chtub 24140 bposlem2 24213 lgs1 24266 colinearalglem4 24939 axsegconlem1 24947 axpaschlem 24970 axcontlem2 24995 axcontlem4 24997 axcontlem7 25000 axcontlem8 25001 constr2spthlem1 25324 2pthon3v 25334 el2spthonot 25598 el2spthonot0 25599 frg2woteq 25788 vc0 26188 vcm 26190 vcnegsubdi2 26194 vcsub4 26195 nvmval2 26264 nvzs 26266 nvmf 26267 nvmdi 26271 nvnegneg 26272 nvsubadd 26276 nvpncan2 26277 nvaddsub4 26282 nvnncan 26284 nvm1 26293 nvdif 26294 nvpi 26295 nvz0 26297 nvmtri 26300 nvabs 26302 nvge0 26303 imsmetlem 26322 4ipval2 26344 ipval3 26345 ipidsq 26349 dipcj 26353 sspmval 26372 ipasslem1 26472 ipasslem2 26473 dipsubdir 26489 hvsubdistr1 26702 shsubcl 26873 shsel3 26968 shunssi 27021 hosubdi 27461 lnopmi 27653 nmophmi 27684 nmopcoi 27748 opsqrlem6 27798 hstle 27883 hst0 27886 mdsl2i 27975 superpos 28007 dmdbr5ati 28075 resvsca 28593 cvmliftphtlem 30040 topdifinffinlem 31750 finixpnum 31930 tan2h 31937 poimirlem3 31943 poimirlem4 31944 poimirlem7 31947 poimirlem16 31956 poimirlem17 31957 poimirlem19 31959 poimirlem20 31960 poimirlem24 31964 poimirlem28 31968 mblfinlem2 31978 mblfinlem4 31980 ismblfin 31981 atlatle 32886 pmaple 33326 dihglblem2N 34862 elnnrabdioph 35650 rabren3dioph 35658 zindbi 35794 expgrowth 36684 binomcxplemnotnn0 36705 trelpss 36808 ltaddneg 37508 etransc 38149 upgredg 39228 uspgrloopnb0 39556 uspgrloopvd2 39557 01wlk 39704 0Trl 39710 pgrple2abl 40203 aacllem 40593 |
Copyright terms: Public domain | W3C validator |