| 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 395 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: mp3an13 1454 mp3an23 1455 mp3anl3 1459 el3v3 3489 opelxp 5721 ov 7577 ovmpoa 7588 ovmpo 7593 frecseq123 8307 oaword1 8590 oneo 8619 oeoalem 8634 oeoelem 8636 nnaword1 8667 nnneo 8693 erov 8854 enrefg 9024 f1imaen 9057 mapxpen 9183 0sdom1dom 9274 acnlem 10088 djucomen 10218 nnadju 10238 infmap 10616 canthnumlem 10688 tskin 10799 tsksn 10800 tsk0 10803 gruxp 10847 gruina 10858 genpprecl 11041 addsrpr 11115 mulsrpr 11116 supsrlem 11151 mulrid 11259 00id 11436 mul02lem1 11437 ltneg 11763 leneg 11766 suble0 11777 div1 11957 nnaddcl 12289 nnmulcl 12290 nnge1 12294 nnsub 12310 2halves 12494 halfaddsub 12499 addltmul 12502 fcdmnn0fsuppg 12586 zleltp1 12668 nnaddm1cl 12675 zextlt 12692 eluzp1p1 12906 uzaddcl 12946 znq 12994 xrre 13211 xrre2 13212 fzshftral 13655 fraclt1 13842 expadd 14145 expmul 14148 sqmul 14159 expubnd 14217 bernneq 14268 faclbnd2 14330 faclbnd6 14338 hashgadd 14416 hashun2 14422 hashunsnggt 14433 hashssdif 14451 hashfun 14476 ccatlcan 14756 ccatrcan 14757 pfx2 14986 shftval3 15115 01sqrexlem1 15281 caubnd2 15396 bpoly2 16093 bpoly3 16094 fsumcube 16096 efexp 16137 efival 16188 cos01gt0 16227 odd2np1 16378 halfleoddlt 16399 omoe 16401 opeo 16402 divalglem5 16434 sqgcd 16599 nn0seqcvgd 16607 prmdvdssq 16755 phiprmpw 16813 eulerthlem2 16819 odzcllem 16830 pythagtriplem15 16867 pythagtriplem17 16869 pcelnn 16908 4sqlem3 16988 fullfunc 17953 fthfunc 17954 prfcl 18248 curf1cl 18273 curfcl 18277 hofcl 18304 odinv 19579 lsmelvalix 19659 dprdval 20023 lsp0 21007 lss0v 21015 zndvds0 21569 frlmlbs 21817 lindfres 21843 lmisfree 21862 coe1scl 22290 ntrin 23069 lpsscls 23149 restperf 23192 txuni2 23573 txopn 23610 elqtop2 23709 xkocnv 23822 ptcmp 24066 xblpnfps 24405 xblpnf 24406 bl2in 24410 unirnblps 24429 unirnbl 24430 blpnfctr 24446 dscopn 24586 bcthlem4 25361 minveclem2 25460 minveclem4 25466 icombl 25599 i1fadd 25730 i1fmul 25731 dvn1 25962 dvexp3 26016 plyconst 26245 plyid 26248 sincosq1eq 26554 sinord 26576 cxpp1 26722 cxpsqrtlem 26744 cxpsqrt 26745 angneg 26846 dcubic 26889 issqf 27179 ppiub 27248 bposlem1 27328 bposlem2 27329 bposlem9 27336 nosupno 27748 nosupfv 27751 noinfno 27763 noinffv 27766 scutval 27845 scutun12 27855 cuteq0 27877 cuteq1 27878 cofcut1 27954 cofcutr 27958 addscut2 28012 sleadd1 28022 addsuniflem 28034 addsasslem1 28036 addsasslem2 28037 negscut2 28072 mulsproplem12 28153 mulscut2 28159 divs1 28229 precsexlem10 28240 precsexlem11 28241 n0s0suc 28345 nnzsubs 28371 zmulscld 28383 axlowdimlem6 28962 axlowdimlem14 28970 axcontlem2 28980 pthdlem2 29788 0ewlk 30133 ipasslem1 30850 ipasslem2 30851 ipasslem11 30859 minvecolem2 30894 minvecolem3 30895 minvecolem4 30899 shsva 31339 h1datomi 31600 lnfnmuli 32063 leopsq 32148 nmopleid 32158 opsqrlem6 32164 pjnmopi 32167 hstle 32249 csmdsymi 32353 atcvatlem 32404 dpfrac1 32874 cshf1o 32947 cycpmconjslem2 33175 rspidlid 33403 elsx 34195 dya2iocnrect 34283 cvmliftphtlem 35322 satfv1 35368 satffunlem1lem2 35408 satffunlem1 35412 wlimeq12 35820 fvray 36142 fvline 36145 tailfb 36378 uncov 37608 tan2h 37619 matunitlindflem1 37623 matunitlindflem2 37624 poimirlem32 37659 mblfinlem4 37667 mbfresfi 37673 mbfposadd 37674 itg2addnc 37681 ftc1anclem5 37704 ftc1anclem8 37707 dvasin 37711 heiborlem7 37824 igenidl 38070 atlatmstc 39320 dihglblem2N 41296 2xp3dxp2ge1d 42242 factwoffsmonot 42243 eldioph4b 42822 diophren 42824 rmxp1 42944 rmyp1 42945 rmxm1 42946 rmym1 42947 dfgric2 47884 gpgov 48001 dig0 48527 i0oii 48817 onetansqsecsq 49280 cotsqcscsq 49281 |
| Copyright terms: Public domain | W3C validator |