![]() |
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 1156 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
4 | 1, 3 | mpi 20 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 |
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 199 df-an 387 df-3an 1115 |
This theorem is referenced by: mp3an13 1582 mp3an23 1583 mp3anl3 1587 opelxp 5379 ov 7041 ovmpt2a 7052 ovmpt2 7057 oaword1 7900 oneo 7929 oeoalem 7944 oeoelem 7946 nnaword1 7977 nnneo 7999 erov 8111 enrefg 8255 f1imaen 8285 mapxpen 8396 acnlem 9185 cdacomen 9319 infmap 9714 canthnumlem 9786 tskin 9897 tsksn 9898 tsk0 9901 gruxp 9945 gruina 9956 genpprecl 10139 addsrpr 10213 mulsrpr 10214 supsrlem 10249 mulid1 10355 00id 10531 mul02lem1 10532 ltneg 10853 leneg 10856 suble0 10867 div1 11042 nnaddcl 11375 nnmulcl 11376 nnmulclOLD 11377 nnge1 11381 nnsub 11396 2halves 11587 halfaddsub 11592 addltmul 11595 zleltp1 11757 nnaddm1cl 11763 zextlt 11780 eluzp1p1 11995 uzaddcl 12027 znq 12076 xrre 12289 xrre2 12290 fzshftral 12723 fraclt1 12899 expadd 13197 expmul 13200 expubnd 13216 sqmul 13221 bernneq 13285 faclbnd2 13372 faclbnd6 13380 hashgadd 13457 hashun2 13463 hashssdif 13490 hashfun 13514 ccatlcan 13808 ccatrcan 13809 pfx2 14069 shftval3 14194 sqrlem1 14361 caubnd2 14475 bpoly2 15161 bpoly3 15162 fsumcube 15164 efexp 15204 efival 15255 cos01gt0 15294 odd2np1 15440 halfleoddlt 15461 omoe 15463 opeo 15464 divalglem5 15495 gcdmultiple 15643 sqgcd 15652 nn0seqcvgd 15657 phiprmpw 15853 eulerthlem2 15859 odzcllem 15869 pythagtriplem15 15906 pythagtriplem17 15908 pcelnn 15946 4sqlem3 16026 xpscfn 16573 fullfunc 16919 fthfunc 16920 prfcl 17197 curf1cl 17222 curfcl 17226 hofcl 17253 odinv 18330 lsmelvalix 18408 dprdval 18757 lsp0 19369 lss0v 19376 coe1scl 20018 zndvds0 20259 frlmlbs 20504 lindfres 20530 lmisfree 20549 ntrin 21237 lpsscls 21317 restperf 21360 txuni2 21740 txopn 21777 elqtop2 21876 xkocnv 21989 ptcmp 22233 xblpnfps 22571 xblpnf 22572 bl2in 22576 unirnblps 22595 unirnbl 22596 blpnfctr 22612 dscopn 22749 bcthlem4 23496 minveclem2 23595 minveclem4 23601 icombl 23731 i1fadd 23862 i1fmul 23863 dvn1 24089 dvexp3 24141 plyconst 24362 plyid 24365 sincosq1eq 24665 sinord 24681 cxpp1 24826 cxpsqrtlem 24848 cxpsqrt 24849 angneg 24944 dcubic 24987 issqf 25276 ppiub 25343 bposlem1 25423 bposlem2 25424 bposlem9 25431 axlowdimlem6 26247 axlowdimlem14 26255 axcontlem2 26265 pthdlem2 27071 0ewlk 27491 ipasslem1 28242 ipasslem2 28243 ipasslem11 28251 minvecolem2 28287 minvecolem3 28288 minvecolem4 28292 shsva 28735 h1datomi 28996 lnfnmuli 29459 leopsq 29544 nmopleid 29554 opsqrlem6 29560 pjnmopi 29563 hstle 29645 csmdsymi 29749 atcvatlem 29800 dpfrac1 30146 elsx 30803 dya2iocnrect 30889 cvmliftphtlem 31846 wlimeq12 32304 frecseq123 32317 nosupno 32389 nosupfv 32392 scutval 32451 scutun12 32457 fvray 32788 fvline 32791 tailfb 32911 uncov 33934 tan2h 33945 matunitlindflem1 33950 matunitlindflem2 33951 poimirlem32 33986 mblfinlem4 33994 mbfresfi 34000 mbfposadd 34001 itg2addnc 34008 ftc1anclem5 34033 ftc1anclem8 34036 dvasin 34040 heiborlem7 34159 igenidl 34405 el3v3 34552 atlatmstc 35395 dihglblem2N 37370 eldioph4b 38220 diophren 38222 rmxp1 38341 rmyp1 38342 rmxm1 38343 rmym1 38344 wepwso 38457 dig0 43248 onetansqsecsq 43401 cotsqcscsq 43402 |
Copyright terms: Public domain | W3C validator |