![]() |
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 1116 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpdan 686 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 206 df-an 396 df-3an 1087 |
This theorem is referenced by: stoic2b 1770 elovmpo 7661 f1oeng 8986 php 9229 nnsdomg 9321 wdomimag 9605 gruuni 10818 genpv 11017 pncan3 11493 mulsubaddmulsub 11703 infssuzle 12940 fzrevral3 13615 flflp1 13799 subsq2 14201 brfi1ind 14487 opfi1ind 14490 ccatws1ls 14610 swrdrlen 14636 pfxpfxid 14686 pfxcctswrd 14687 2cshwid 14791 caubnd 15332 dvdsmul1 16249 dvdsmul2 16250 hashbcval 16965 setsvalg 17129 ressval 17206 restval 17402 mrelatglb0 18547 imasmnd2 18725 efmndov 18827 qusinv 19139 ghminv 19171 gsmsymgrfixlem1 19376 gsmsymgreqlem2 19380 gexod 19535 lsmvalx 19588 rngrz 20100 imasring 20260 irredneg 20363 01eq0ring 20461 ocvin 21600 frlmiscvec 21777 evlrhm 22036 gsumsmonply1 22220 mat1mhm 22380 marrepfval 22456 marrepval0 22457 marepvfval 22461 marepvval0 22462 1elcpmat 22611 m2cpminv0 22657 idpm2idmp 22697 chfacfscmulgsum 22756 chfacfpmmulgsum 22760 restin 23064 qtopval 23593 elqtop3 23601 elfm3 23848 flimval 23861 nmge0 24520 nmeq0 24521 nminv 24524 nmo0 24646 0nghm 24652 coemulhi 26182 isosctrlem2 26745 divsqrtsumlem 26906 2lgsoddprmlem4 27342 0uhgrrusgr 29386 frgruhgr0v 30068 nvge0 30477 nvnd 30492 dip0r 30521 dip0l 30522 nmoo0 30595 hi2eq 30909 wrdsplex 32656 resvval 33033 unitdivcld 33497 signspval 34179 satfv0 34963 ltflcei 37076 elghomlem1OLD 37353 rngorz 37391 rngonegmn1l 37409 rngonegmn1r 37410 igenval 37529 xrnidresex 37874 xrncnvepresex 37875 lfl0 38532 olj01 38692 olm11 38694 hl2at 38873 pmapeq0 39234 trlcl 39632 trlle 39652 tendoid 40241 tendo0plr 40260 tendoipl2 40266 erngmul 40274 erngmul-rN 40282 dvamulr 40480 dvavadd 40483 dvhmulr 40554 cdlemm10N 40586 repncan3 41929 pellfund14 42309 mendmulr 42603 onnog 42850 fmuldfeq 44962 stoweidlem19 45398 stoweidlem26 45405 addsubeq0 46667 prelspr 46817 lincval1 47478 |
Copyright terms: Public domain | W3C validator |