![]() |
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 1122 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
4 | 1, 3 | mpi 20 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: mp3an13 1453 mp3an23 1454 mp3anl3 1458 opelxp 5670 ov 7500 ovmpoa 7511 ovmpo 7516 frecseq123 8214 oaword1 8500 oneo 8529 oeoalem 8544 oeoelem 8546 nnaword1 8577 nnneo 8602 erov 8754 enrefg 8925 f1imaen 8957 mapxpen 9088 0sdom1dom 9183 acnlem 9985 djucomen 10114 nnadju 10134 infmap 10513 canthnumlem 10585 tskin 10696 tsksn 10697 tsk0 10700 gruxp 10744 gruina 10755 genpprecl 10938 addsrpr 11012 mulsrpr 11013 supsrlem 11048 mulid1 11154 00id 11331 mul02lem1 11332 ltneg 11656 leneg 11659 suble0 11670 div1 11845 nnaddcl 12177 nnmulcl 12178 nnge1 12182 nnsub 12198 2halves 12382 halfaddsub 12387 addltmul 12390 fcdmnn0fsuppg 12473 zleltp1 12555 nnaddm1cl 12561 zextlt 12578 eluzp1p1 12792 uzaddcl 12830 znq 12878 xrre 13089 xrre2 13090 fzshftral 13530 fraclt1 13708 expadd 14011 expmul 14014 sqmul 14025 expubnd 14083 bernneq 14133 faclbnd2 14192 faclbnd6 14200 hashgadd 14278 hashun2 14284 hashunsnggt 14295 hashssdif 14313 hashfun 14338 ccatlcan 14607 ccatrcan 14608 pfx2 14837 shftval3 14962 01sqrexlem1 15128 caubnd2 15243 bpoly2 15941 bpoly3 15942 fsumcube 15944 efexp 15984 efival 16035 cos01gt0 16074 odd2np1 16224 halfleoddlt 16245 omoe 16247 opeo 16248 divalglem5 16280 sqgcd 16442 nn0seqcvgd 16447 prmdvdssq 16595 phiprmpw 16649 eulerthlem2 16655 odzcllem 16665 pythagtriplem15 16702 pythagtriplem17 16704 pcelnn 16743 4sqlem3 16823 fullfunc 17794 fthfunc 17795 prfcl 18092 curf1cl 18118 curfcl 18122 hofcl 18149 odinv 19344 lsmelvalix 19424 dprdval 19783 lsp0 20473 lss0v 20480 zndvds0 20960 frlmlbs 21206 lindfres 21232 lmisfree 21251 coe1scl 21661 ntrin 22415 lpsscls 22495 restperf 22538 txuni2 22919 txopn 22956 elqtop2 23055 xkocnv 23168 ptcmp 23412 xblpnfps 23751 xblpnf 23752 bl2in 23756 unirnblps 23775 unirnbl 23776 blpnfctr 23792 dscopn 23932 bcthlem4 24694 minveclem2 24793 minveclem4 24799 icombl 24931 i1fadd 25062 i1fmul 25063 dvn1 25293 dvexp3 25345 plyconst 25570 plyid 25573 sincosq1eq 25872 sinord 25893 cxpp1 26038 cxpsqrtlem 26060 cxpsqrt 26061 angneg 26156 dcubic 26199 issqf 26488 ppiub 26555 bposlem1 26635 bposlem2 26636 bposlem9 26643 nosupno 27054 nosupfv 27057 noinfno 27069 noinffv 27072 scutval 27142 scutun12 27152 cuteq0 27174 cofcut1 27242 cofcutr 27246 sleadd1 27301 addsunif 27313 addsasslem1 27314 addsasslem2 27315 negscut2 27341 axlowdimlem6 27899 axlowdimlem14 27907 axcontlem2 27917 pthdlem2 28719 0ewlk 29061 ipasslem1 29776 ipasslem2 29777 ipasslem11 29785 minvecolem2 29820 minvecolem3 29821 minvecolem4 29825 shsva 30265 h1datomi 30526 lnfnmuli 30989 leopsq 31074 nmopleid 31084 opsqrlem6 31090 pjnmopi 31093 hstle 31175 csmdsymi 31279 atcvatlem 31330 dpfrac1 31751 cshf1o 31819 cycpmconjslem2 32007 rspidlid 32166 elsx 32796 dya2iocnrect 32884 cvmliftphtlem 33914 satfv1 33960 satffunlem1lem2 34000 satffunlem1 34004 wlimeq12 34397 fvray 34729 fvline 34732 tailfb 34852 uncov 36062 tan2h 36073 matunitlindflem1 36077 matunitlindflem2 36078 poimirlem32 36113 mblfinlem4 36121 mbfresfi 36127 mbfposadd 36128 itg2addnc 36135 ftc1anclem5 36158 ftc1anclem8 36161 dvasin 36165 heiborlem7 36279 igenidl 36525 el3v3 36683 atlatmstc 37784 dihglblem2N 39760 2xp3dxp2ge1d 40617 factwoffsmonot 40618 eldioph4b 41137 diophren 41139 rmxp1 41259 rmyp1 41260 rmxm1 41261 rmym1 41262 dig0 46699 i0oii 46959 onetansqsecsq 47213 cotsqcscsq 47214 |
Copyright terms: Public domain | W3C validator |