![]() |
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 1116 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 700 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 206 df-an 396 df-3an 1087 |
This theorem is referenced by: mp3anl2 1453 vtoclegft 3571 tz7.7 6395 ordin 6399 onfr 6408 fprresex 8316 wfrlem14OLD 8343 wfrlem17OLD 8346 tfrlem11 8409 phplem2 9233 epfrs 9755 zorng 10528 tsk2 10789 tskcard 10805 gruina 10842 muladd11 11415 00id 11420 ltaddneg 11460 negsub 11539 subneg 11540 muleqadd 11889 diveq1 11936 conjmul 11962 recp1lt1 12143 nnsub 12287 addltmul 12479 nnunb 12499 zltp1le 12643 gtndiv 12670 eluzp1m1 12879 zbtwnre 12961 rebtwnz 12962 xnn0le2is012 13258 supxrbnd 13340 divelunit 13504 fznatpl1 13588 flbi2 13815 fldiv 13858 modid 13894 modm1p1mod0 13920 fzen2 13967 nn0ennn 13977 seqshft2 14026 seqf1olem1 14039 ser1const 14056 sq01 14220 expnbnd 14227 faclbnd3 14284 faclbnd5 14290 hashunsng 14384 hashunsngx 14385 hashxplem 14425 ccatrid 14570 ccats1val1 14609 ccat2s1fst 14622 sgnn 15074 01sqrexlem2 15223 01sqrexlem7 15228 leabs 15279 abs2dif 15312 cvgrat 15862 cos2t 16155 sin01gt0 16167 cos01gt0 16168 demoivre 16177 demoivreALT 16178 rpnnen2lem5 16195 rpnnen2lem12 16202 omeo 16343 gcd0id 16494 sqgcd 16536 isprm3 16654 eulerthlem2 16751 pczpre 16816 pcrec 16827 ressress 17229 mulgm1 19049 unitgrpid 20324 mdet0pr 22507 m2detleib 22546 cmpcov2 23307 ufileu 23836 tgpconncompeqg 24029 itg2ge0 25678 mdegldg 26015 abssinper 26468 ppiub 27150 chtub 27158 bposlem2 27231 lgs1 27287 cofcutr 27857 negsbdaylem 27981 precsexlem10 28127 n0sbday 28230 remulscllem1 28241 colinearalglem4 28733 axsegconlem1 28741 axpaschlem 28764 axcontlem2 28789 axcontlem4 28791 axcontlem7 28794 axcontlem8 28795 funvtxval 28844 funiedgval 28845 vc0 30397 vcm 30399 nvmval2 30466 nvmf 30468 nvmdi 30471 nvnegneg 30472 nvpncan2 30476 nvaddsub4 30480 nvm1 30488 nvdif 30489 nvpi 30490 nvz0 30491 nvmtri 30494 nvabs 30495 nvge0 30496 imsmetlem 30513 4ipval2 30531 ipval3 30532 ipidsq 30533 dipcj 30537 sspmval 30556 ipasslem1 30654 ipasslem2 30655 dipsubdir 30671 hvsubdistr1 30872 shsubcl 31043 shsel3 31138 shunssi 31191 hosubdi 31631 lnopmi 31823 nmophmi 31854 nmopcoi 31918 opsqrlem6 31968 hstle 32053 hst0 32056 mdsl2i 32145 superpos 32177 dmdbr5ati 32245 f1rnen 32427 resvsca 33054 pthhashvtx 34737 cvmliftphtlem 34927 topdifinffinlem 36826 finixpnum 37078 tan2h 37085 poimirlem3 37096 poimirlem4 37097 poimirlem7 37100 poimirlem16 37109 poimirlem17 37110 poimirlem19 37112 poimirlem20 37113 poimirlem24 37117 poimirlem28 37121 mblfinlem2 37131 mblfinlem4 37133 ismblfin 37134 el3v2 37693 atlatle 38792 pmaple 39234 dihglblem2N 40767 expgcd 41894 sn-ltaddneg 41997 elnnrabdioph 42227 rabren3dioph 42235 zindbi 42367 expgrowth 43772 binomcxplemnotnn0 43793 trelpss 43892 etransc 45671 mogoldbb 47125 pgrple2abl 47429 aacllem 48234 |
Copyright terms: Public domain | W3C validator |