| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mpd3an3 | Structured version Visualization version GIF version | ||
| Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.) |
| Ref | Expression |
|---|---|
| mpd3an3.2 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
| mpd3an3.3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| mpd3an3 | ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpd3an3.2 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
| 2 | mpd3an3.3 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 3 | 2 | 3expa 1119 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
| 4 | 1, 3 | mpdan 687 | 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: stoic2b 1775 elovmpo 7678 f1oeng 9011 php 9247 nnsdomg 9335 wdomimag 9627 gruuni 10840 genpv 11039 pncan3 11516 mulsubaddmulsub 11727 infssuzle 12973 fzrevral3 13654 flflp1 13847 subsq2 14250 brfi1ind 14548 opfi1ind 14551 ccatws1ls 14671 swrdrlen 14697 pfxpfxid 14747 pfxcctswrd 14748 2cshwid 14852 caubnd 15397 dvdsmul1 16315 dvdsmul2 16316 hashbcval 17040 setsvalg 17203 ressval 17277 restval 17471 mrelatglb0 18606 imasmnd2 18787 efmndov 18894 qusinv 19208 ghminv 19241 gsmsymgrfixlem1 19445 gsmsymgreqlem2 19449 gexod 19604 lsmvalx 19657 rngrz 20163 imasring 20327 irredneg 20430 01eq0ring 20530 ocvin 21692 frlmiscvec 21869 evlrhm 22120 gsumsmonply1 22311 mat1mhm 22490 marrepfval 22566 marrepval0 22567 marepvfval 22571 marepvval0 22572 1elcpmat 22721 m2cpminv0 22767 idpm2idmp 22807 chfacfscmulgsum 22866 chfacfpmmulgsum 22870 restin 23174 qtopval 23703 elqtop3 23711 elfm3 23958 flimval 23971 nmge0 24630 nmeq0 24631 nminv 24634 nmo0 24756 0nghm 24762 coemulhi 26293 isosctrlem2 26862 divsqrtsumlem 27023 2lgsoddprmlem4 27459 0uhgrrusgr 29596 frgruhgr0v 30283 nvge0 30692 nvnd 30707 dip0r 30736 dip0l 30737 nmoo0 30810 hi2eq 31124 wrdsplex 32920 resvval 33353 unitdivcld 33900 signspval 34567 satfv0 35363 ltflcei 37615 elghomlem1OLD 37892 rngorz 37930 rngonegmn1l 37948 rngonegmn1r 37949 igenval 38068 xrnidresex 38408 xrncnvepresex 38409 lfl0 39066 olj01 39226 olm11 39228 hl2at 39407 pmapeq0 39768 trlcl 40166 trlle 40186 tendoid 40775 tendo0plr 40794 tendoipl2 40800 erngmul 40808 erngmul-rN 40816 dvamulr 41014 dvavadd 41017 dvhmulr 41088 cdlemm10N 41120 repncan3 42413 pellfund14 42909 mendmulr 43196 onnog 43442 fmuldfeq 45598 stoweidlem19 46034 stoweidlem26 46041 addsubeq0 47308 zp1modne 47348 prelspr 47473 lincval1 48336 |
| Copyright terms: Public domain | W3C validator |