![]() |
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 1114 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
4 | 1, 3 | mpi 20 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1071 |
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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: mp3an13 1563 mp3an23 1564 mp3anl3 1568 opelxp 5286 ov 6927 ovmpt2a 6938 ovmpt2 6943 oaword1 7786 oneo 7815 oeoalem 7830 oeoelem 7832 nnaword1 7863 nnneo 7885 erov 7997 enrefg 8141 f1imaen 8171 mapxpen 8282 acnlem 9071 cdacomen 9205 infmap 9600 canthnumlem 9672 tskin 9783 tsksn 9784 tsk0 9787 gruxp 9831 gruina 9842 genpprecl 10025 addsrpr 10098 mulsrpr 10099 supsrlem 10134 mulid1 10239 00id 10413 mul02lem1 10414 ltneg 10730 leneg 10733 suble0 10744 div1 10918 nnaddcl 11244 nnmulcl 11245 nnge1 11248 nnsub 11261 2halves 11462 halfaddsub 11467 addltmul 11470 zleltp1 11630 nnaddm1cl 11636 zextlt 11653 eluzp1p1 11914 uzaddcl 11946 znq 11995 xrre 12205 xrre2 12206 fzshftral 12635 fraclt1 12811 expadd 13109 expmul 13112 expubnd 13128 sqmul 13133 bernneq 13197 faclbnd2 13282 faclbnd6 13290 hashgadd 13368 hashun2 13374 hashssdif 13402 hashfun 13426 ccatlcan 13681 ccatrcan 13682 shftval3 14024 sqrlem1 14191 caubnd2 14305 bpoly2 14994 bpoly3 14995 fsumcube 14997 efexp 15037 efival 15088 cos01gt0 15127 odd2np1 15273 halfleoddlt 15294 omoe 15296 opeo 15297 divalglem5 15328 gcdmultiple 15477 sqgcd 15486 nn0seqcvgd 15491 phiprmpw 15688 eulerthlem2 15694 odzcllem 15704 pythagtriplem15 15741 pythagtriplem17 15743 pcelnn 15781 4sqlem3 15861 xpscfn 16427 fullfunc 16773 fthfunc 16774 prfcl 17051 curf1cl 17076 curfcl 17080 hofcl 17107 odinv 18185 lsmelvalix 18263 dprdval 18610 lsp0 19222 lss0v 19229 coe1scl 19872 zndvds0 20114 frlmlbs 20353 lindfres 20379 lmisfree 20398 ntrin 21086 lpsscls 21166 restperf 21209 txuni2 21589 txopn 21626 elqtop2 21725 xkocnv 21838 ptcmp 22082 xblpnfps 22420 xblpnf 22421 bl2in 22425 unirnblps 22444 unirnbl 22445 blpnfctr 22461 dscopn 22598 bcthlem4 23343 minveclem2 23416 minveclem4 23422 icombl 23552 i1fadd 23682 i1fmul 23683 dvn1 23909 dvexp3 23961 plyconst 24182 plyid 24185 sincosq1eq 24485 sinord 24501 cxpp1 24647 cxpsqrtlem 24669 cxpsqrt 24670 angneg 24754 dcubic 24794 issqf 25083 ppiub 25150 bposlem1 25230 bposlem2 25231 bposlem9 25238 axlowdimlem6 26048 axlowdimlem14 26056 axcontlem2 26066 structgrssvtxlemOLD 26136 pthdlem2 26899 0ewlk 27294 ipasslem1 28026 ipasslem2 28027 ipasslem11 28035 minvecolem2 28071 minvecolem3 28072 minvecolem4 28076 shsva 28519 h1datomi 28780 lnfnmuli 29243 leopsq 29328 nmopleid 29338 opsqrlem6 29344 pjnmopi 29347 hstle 29429 csmdsymi 29533 atcvatlem 29584 dpfrac1 29939 dpfrac1OLD 29940 elsx 30597 dya2iocnrect 30683 cvmliftphtlem 31637 wlimeq12 32101 frecseq123 32114 nosupno 32186 nosupfv 32189 scutval 32248 scutun12 32254 fvray 32585 fvline 32588 tailfb 32709 uncov 33723 tan2h 33734 matunitlindflem1 33738 matunitlindflem2 33739 poimirlem32 33774 mblfinlem4 33782 mbfresfi 33788 mbfposadd 33789 itg2addnc 33796 ftc1anclem5 33821 ftc1anclem8 33824 dvasin 33828 heiborlem7 33948 igenidl 34194 el3v3 34335 atlatmstc 35128 dihglblem2N 37104 eldioph4b 37901 diophren 37903 rmxp1 38023 rmyp1 38024 rmxm1 38025 rmym1 38026 wepwso 38139 pfx2 41940 dig0 42928 onetansqsecsq 43033 cotsqcscsq 43034 |
Copyright terms: Public domain | W3C validator |