Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mp3an2 | Structured version Visualization version GIF 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 1110 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 697 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: mp3anl2 1447 tz7.7 6210 ordin 6214 onfr 6223 wfrlem14 7957 wfrlem17 7960 tfrlem11 8013 epfrs 9161 zorng 9914 tsk2 10175 tskcard 10191 gruina 10228 muladd11 10798 00id 10803 ltaddneg 10843 negsub 10922 subneg 10923 muleqadd 11272 diveq1 11319 conjmul 11345 recp1lt1 11526 nnsub 11669 addltmul 11861 nnunb 11881 zltp1le 12020 gtndiv 12047 eluzp1m1 12256 zbtwnre 12334 rebtwnz 12335 xnn0le2is012 12627 supxrbnd 12709 divelunit 12868 fznatpl1 12949 flbi2 13175 fldiv 13216 modid 13252 modm1p1mod0 13278 fzen2 13325 nn0ennn 13335 seqshft2 13384 seqf1olem1 13397 ser1const 13414 sq01 13574 expnbnd 13581 faclbnd3 13640 faclbnd5 13646 hashunsng 13741 hashunsngx 13742 hashxplem 13782 ccatrid 13929 ccats1val1 13969 ccat2s1fst 13988 sgnn 14441 sqrlem2 14591 sqrlem7 14596 leabs 14647 abs2dif 14680 cvgrat 15227 cos2t 15519 sin01gt0 15531 cos01gt0 15532 demoivre 15541 demoivreALT 15542 rpnnen2lem5 15559 rpnnen2lem12 15566 omeo 15703 gcd0id 15855 sqgcd 15897 isprm3 16015 eulerthlem2 16107 pczpre 16172 pcrec 16183 ressress 16550 mulgm1 18186 unitgrpid 19348 mdet0pr 21129 m2detleib 21168 cmpcov2 21926 ufileu 22455 tgpconncompeqg 22647 itg2ge0 24263 mdegldg 24587 abssinper 25033 ppiub 25707 chtub 25715 bposlem2 25788 lgs1 25844 colinearalglem4 26622 axsegconlem1 26630 axpaschlem 26653 axcontlem2 26678 axcontlem4 26680 axcontlem7 26683 axcontlem8 26684 funvtxval 26730 funiedgval 26731 vc0 28278 vcm 28280 nvmval2 28347 nvmf 28349 nvmdi 28352 nvnegneg 28353 nvpncan2 28357 nvaddsub4 28361 nvm1 28369 nvdif 28370 nvpi 28371 nvz0 28372 nvmtri 28375 nvabs 28376 nvge0 28377 imsmetlem 28394 4ipval2 28412 ipval3 28413 ipidsq 28414 dipcj 28418 sspmval 28437 ipasslem1 28535 ipasslem2 28536 dipsubdir 28552 hvsubdistr1 28753 shsubcl 28924 shsel3 29019 shunssi 29072 hosubdi 29512 lnopmi 29704 nmophmi 29735 nmopcoi 29799 opsqrlem6 29849 hstle 29934 hst0 29937 mdsl2i 30026 superpos 30058 dmdbr5ati 30126 f1rnen 30302 resvsca 30830 pthhashvtx 32271 cvmliftphtlem 32461 topdifinffinlem 34510 finixpnum 34758 tan2h 34765 poimirlem3 34776 poimirlem4 34777 poimirlem7 34780 poimirlem16 34789 poimirlem17 34790 poimirlem19 34792 poimirlem20 34793 poimirlem24 34797 poimirlem28 34801 mblfinlem2 34811 mblfinlem4 34813 ismblfin 34814 el3v2 35374 atlatle 36336 pmaple 36777 dihglblem2N 38310 expgcd 39061 elnnrabdioph 39282 rabren3dioph 39290 zindbi 39421 expgrowth 40544 binomcxplemnotnn0 40565 trelpss 40664 etransc 42445 mogoldbb 43827 pgrple2abl 44341 aacllem 44830 |
Copyright terms: Public domain | W3C validator |