![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mp3an3 | Structured version Visualization version GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an3.1 | ⊢ 𝜒 |
mp3an3.2 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an3 | ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an3.1 | . 2 ⊢ 𝜒 | |
2 | mp3an3.2 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 2 | 3expia 1120 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
4 | 1, 3 | mpi 20 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: mp3an13 1451 mp3an23 1452 mp3anl3 1456 opelxp 5712 ov 7555 ovmpoa 7566 ovmpo 7571 frecseq123 8273 oaword1 8558 oneo 8587 oeoalem 8602 oeoelem 8604 nnaword1 8635 nnneo 8660 erov 8814 enrefg 8986 f1imaen 9018 mapxpen 9149 0sdom1dom 9244 acnlem 10049 djucomen 10178 nnadju 10198 infmap 10577 canthnumlem 10649 tskin 10760 tsksn 10761 tsk0 10764 gruxp 10808 gruina 10819 genpprecl 11002 addsrpr 11076 mulsrpr 11077 supsrlem 11112 mulrid 11219 00id 11396 mul02lem1 11397 ltneg 11721 leneg 11724 suble0 11735 div1 11910 nnaddcl 12242 nnmulcl 12243 nnge1 12247 nnsub 12263 2halves 12447 halfaddsub 12452 addltmul 12455 fcdmnn0fsuppg 12538 zleltp1 12620 nnaddm1cl 12626 zextlt 12643 eluzp1p1 12857 uzaddcl 12895 znq 12943 xrre 13155 xrre2 13156 fzshftral 13596 fraclt1 13774 expadd 14077 expmul 14080 sqmul 14091 expubnd 14149 bernneq 14199 faclbnd2 14258 faclbnd6 14266 hashgadd 14344 hashun2 14350 hashunsnggt 14361 hashssdif 14379 hashfun 14404 ccatlcan 14675 ccatrcan 14676 pfx2 14905 shftval3 15030 01sqrexlem1 15196 caubnd2 15311 bpoly2 16008 bpoly3 16009 fsumcube 16011 efexp 16051 efival 16102 cos01gt0 16141 odd2np1 16291 halfleoddlt 16312 omoe 16314 opeo 16315 divalglem5 16347 sqgcd 16509 nn0seqcvgd 16514 prmdvdssq 16662 phiprmpw 16716 eulerthlem2 16722 odzcllem 16732 pythagtriplem15 16769 pythagtriplem17 16771 pcelnn 16810 4sqlem3 16890 fullfunc 17866 fthfunc 17867 prfcl 18165 curf1cl 18191 curfcl 18195 hofcl 18222 odinv 19477 lsmelvalix 19557 dprdval 19921 lsp0 20852 lss0v 20859 zndvds0 21415 frlmlbs 21661 lindfres 21687 lmisfree 21706 coe1scl 22128 ntrin 22884 lpsscls 22964 restperf 23007 txuni2 23388 txopn 23425 elqtop2 23524 xkocnv 23637 ptcmp 23881 xblpnfps 24220 xblpnf 24221 bl2in 24225 unirnblps 24244 unirnbl 24245 blpnfctr 24261 dscopn 24401 bcthlem4 25174 minveclem2 25273 minveclem4 25279 icombl 25412 i1fadd 25543 i1fmul 25544 dvn1 25775 dvexp3 25829 plyconst 26057 plyid 26060 sincosq1eq 26361 sinord 26382 cxpp1 26527 cxpsqrtlem 26549 cxpsqrt 26550 angneg 26648 dcubic 26691 issqf 26980 ppiub 27049 bposlem1 27129 bposlem2 27130 bposlem9 27137 nosupno 27548 nosupfv 27551 noinfno 27563 noinffv 27566 scutval 27645 scutun12 27655 cuteq0 27677 cuteq1 27678 cofcut1 27752 cofcutr 27756 addscut2 27808 sleadd1 27818 addsuniflem 27830 addsasslem1 27832 addsasslem2 27833 negscut2 27864 mulsproplem12 27939 mulscut2 27945 divs1 28015 precsexlem10 28026 precsexlem11 28027 axlowdimlem6 28637 axlowdimlem14 28645 axcontlem2 28655 pthdlem2 29457 0ewlk 29799 ipasslem1 30516 ipasslem2 30517 ipasslem11 30525 minvecolem2 30560 minvecolem3 30561 minvecolem4 30565 shsva 31005 h1datomi 31266 lnfnmuli 31729 leopsq 31814 nmopleid 31824 opsqrlem6 31830 pjnmopi 31833 hstle 31915 csmdsymi 32019 atcvatlem 32070 dpfrac1 32490 cshf1o 32558 cycpmconjslem2 32749 rspidlid 32926 elsx 33655 dya2iocnrect 33743 cvmliftphtlem 34771 satfv1 34817 satffunlem1lem2 34857 satffunlem1 34861 wlimeq12 35260 fvray 35582 fvline 35585 tailfb 35725 uncov 36932 tan2h 36943 matunitlindflem1 36947 matunitlindflem2 36948 poimirlem32 36983 mblfinlem4 36991 mbfresfi 36997 mbfposadd 36998 itg2addnc 37005 ftc1anclem5 37028 ftc1anclem8 37031 dvasin 37035 heiborlem7 37148 igenidl 37394 el3v3 37552 atlatmstc 38652 dihglblem2N 40628 2xp3dxp2ge1d 41488 factwoffsmonot 41489 eldioph4b 42011 diophren 42013 rmxp1 42133 rmyp1 42134 rmxm1 42135 rmym1 42136 dig0 47453 i0oii 47713 onetansqsecsq 47967 cotsqcscsq 47968 |
Copyright terms: Public domain | W3C validator |