![]() |
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 1108 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpdan 677 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ 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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: stoic2b 1819 elovmpt2 7156 f1oeng 8260 wdomimag 8781 cdaval 9327 gruuni 9957 genpv 10156 pncan3 10630 mulsubaddmulsub 10839 infssuzle 12078 fzrevral3 12745 flflp1 12927 subsq2 13292 brfi1ind 13595 opfi1ind 13598 ccatws1ls 13723 swrdrlen 13754 swrd0swrdidOLD 13821 pfxpfxid 13822 pfxcctswrd 13823 2cshwid 13965 caubnd 14505 dvdsmul1 15410 dvdsmul2 15411 hashbcval 16110 setsvalg 16284 ressval 16323 restval 16473 mrelatglb0 17571 imasmnd2 17713 qusinv 18037 ghminv 18051 symgov 18193 gexod 18385 lsmvalx 18438 ringrz 18975 imasring 19006 irredneg 19097 evlrhm 19921 gsumsmonply1 20069 ocvin 20417 frlmiscvec 20592 mat1mhm 20695 marrepfval 20771 marrepval0 20772 marepvfval 20776 marepvval0 20777 1elcpmat 20927 m2cpminv0 20973 idpm2idmp 21013 chfacfscmulgsum 21072 chfacfpmmulgsum 21076 restin 21378 qtopval 21907 elqtop3 21915 elfm3 22162 flimval 22175 nmge0 22829 nmeq0 22830 nminv 22833 nmo0 22947 0nghm 22953 coemulhi 24447 isosctrlem2 24997 divsqrtsumlem 25158 2lgsoddprmlem4 25592 0uhgrrusgr 26926 frgruhgr0v 27671 nvge0 28100 nvnd 28115 dip0r 28144 dip0l 28145 nmoo0 28218 hi2eq 28534 resvval 30389 unitdivcld 30545 wrdsplex 31217 signspval 31229 ltflcei 34022 elghomlem1OLD 34308 rngorz 34346 rngonegmn1l 34364 rngonegmn1r 34365 igenval 34484 xrnidresex 34793 xrncnvepresex 34794 lfl0 35219 olj01 35379 olm11 35381 hl2at 35559 pmapeq0 35920 trlcl 36318 trlle 36338 tendoid 36927 tendo0plr 36946 tendoipl2 36952 erngmul 36960 erngmul-rN 36968 dvamulr 37166 dvavadd 37169 dvhmulr 37240 cdlemm10N 37272 repncan3 38192 pellfund14 38422 mendmulr 38717 fmuldfeq 40723 stoweidlem19 41163 stoweidlem26 41170 addsubeq0 42338 prelspr 42425 lincval1 43223 |
Copyright terms: Public domain | W3C validator |