| 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 1136 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
| 4 | 1, 3 | mpanl2 714 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This proof depends on definitions: df-bi 210 df-an 402 df-3an 1105 |
| This theorem is used by: mp3anl2 1485 vtoclegft 3546 tz7.7 6387 ordin 6392 onfr 6401 fprresex 8313 tfrlem11 8381 phplem2 9203 epfrs 9714 zorng 10510 tsk2 10778 tskcard 10794 gruina 10831 muladd11 11408 00id 11413 ltaddneg 11454 negsub 11534 subneg 11535 muleqadd 11886 diveq0 11910 diveq1 11929 conjmul 11960 recp1lt1 12141 nnsub 12308 addltmul 12508 nnunb 12528 zltp1le 12672 gtndiv 12702 eluzp1m1 12917 zbtwnre 12999 rebtwnz 13000 xnn0le2is012 13302 supxrbnd 13384 divelunit 13551 fznatpl1 13637 flbi2 13882 fldiv 13925 modid 13961 modm1p1mod0 13990 fzen2 14037 nn0ennn 14047 seqshft2 14096 seqf1olem1 14109 ser1const 14126 sq01 14293 expnbnd 14300 faclbnd3 14360 faclbnd5 14366 hashunsng 14460 hashunsngx 14461 hashxplem 14502 ccatrid 14657 ccats1val1 14698 ccat2s1fst 14711 sgnn 15171 01sqrexlem2 15334 01sqrexlem7 15339 leabs 15390 abs2dif 15424 cvgrat 15976 cos2t 16272 sin01gt0 16284 cos01gt0 16285 demoivre 16294 demoivreALT 16295 rpnnen2lem5 16312 rpnnen2lem12 16319 omeo 16462 gcd0id 16615 sqgcd 16658 expgcd 16659 isprm3 16779 eulerthlem2 16879 pczpre 16945 pcrec 16956 ressress 17345 mulgm1 19223 unitgrpid 20532 mdet0pr 22820 m2detleib 22859 cmpcov2 23621 ufileu 24151 tgpconncompeqg 24344 itg2ge0 25969 mdegldg 26298 abssinper 26766 ppiub 27448 chtub 27456 bposlem2 27529 lgs1 27585 cofcutr 28197 addbday 28291 negbdaylem 28329 precsexlem10 28489 oncutlt 28537 n0bday 28625 bdayn0p1 28642 eucliddivs 28649 nnzs 28659 bdaypw2n0bndlem 28736 zz12s 28748 remulscllem1 28773 colinearalglem4 29374 axsegconlem1 29382 axpaschlem 29405 axcontlem2 29430 axcontlem4 29432 axcontlem7 29435 axcontlem8 29436 funvtxval 29483 funiedgval 29484 pthhashvtx 30202 vc0 31063 vcm 31065 nvmval2 31132 nvmf 31134 nvmdi 31137 nvnegneg 31138 nvpncan2 31142 nvaddsub4 31146 nvm1 31154 nvdif 31155 nvpi 31156 nvz0 31157 nvmtri 31160 nvabs 31161 nvge0 31162 imsmetlem 31179 4ipval2 31197 ipval3 31198 ipidsq 31199 dipcj 31203 sspmval 31222 ipasslem1 31320 ipasslem2 31321 dipsubdir 31337 hvsubdistr1 31538 shsubcl 31709 shsel3 31804 shunssi 31857 hosubdi 32297 lnopmi 32489 nmophmi 32520 nmopcoi 32584 opsqrlem6 32634 hstle 32719 hst0 32722 mdsl2i 32811 superpos 32843 dmdbr5ati 32911 f1rnen 33109 resvsca 33780 noinfepfnregs 35666 cvmliftphtlem 35904 topdifinffinlem 38109 finixpnum 38367 tan2h 38374 poimirlem3 38380 poimirlem4 38381 poimirlem7 38384 poimirlem16 38393 poimirlem17 38394 poimirlem19 38396 poimirlem20 38397 poimirlem24 38401 poimirlem28 38405 mblfinlem2 38415 mblfinlem4 38417 ismblfin 38418 el3v2 38987 atlatle 40201 pmaple 40642 dihglblem2N 42175 sn-ltaddneg 43350 elnnrabdioph 43656 rabren3dioph 43664 zindbi 43795 expgrowth 45167 binomcxplemnotnn0 45188 trelpss 45285 etransc 47119 mogoldbb 48709 pgrple2abl 49303 aacllem 50780 |
| Copyright terms: Public domain | W3C validator |