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 1257 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpdan 699 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: stoic2b 1691 elovmpt2 6777 f1oeng 7860 wdomimag 8375 cdaval 8875 gruuni 9501 genpv 9700 infssuzle 11647 fzrevral3 12296 flflp1 12470 subsq2 12835 brfi1ind 13136 opfi1ind 13139 brfi1indOLD 13142 opfi1indOLD 13145 ccatws1ls 13262 swrdrlen 13287 swrd0swrdid 13316 2cshwid 13411 caubnd 13946 dvdsmul1 14841 dvdsmul2 14842 hashbcval 15544 setsvalg 15719 ressval 15754 restval 15910 mrelatglb0 17008 imasmnd2 17150 qusinv 17476 ghminv 17490 symgov 17633 gexod 17824 lsmvalx 17877 ringrz 18411 imasring 18442 irredneg 18533 evlrhm 19346 gsumsmonply1 19494 ocvin 19837 frlmiscvec 20007 mat1mhm 20109 marrepfval 20185 marrepval0 20186 marepvfval 20190 marepvval0 20191 1elcpmat 20339 m2cpminv0 20385 idpm2idmp 20425 chfacfscmulgsum 20484 chfacfpmmulgsum 20488 restin 20780 qtopval 21308 elqtop3 21316 elfm3 21564 flimval 21577 nmge0 22231 nmeq0 22232 nminv 22235 nmo0 22349 0nghm 22355 coemulhi 23814 isosctrlem2 24349 divsqrtsumlem 24506 2lgsoddprmlem4 24940 nvge0 26912 nvnd 26927 dip0r 26956 dip0l 26957 nmoo0 27030 hi2eq 27346 resvval 29158 unitdivcld 29275 signspval 29955 ltflcei 32567 elghomlem1OLD 32854 rngorz 32892 rngonegmn1l 32910 rngonegmn1r 32911 igenval 33030 lfl0 33370 olj01 33530 olm11 33532 hl2at 33709 pmapeq0 34070 trlcl 34469 trlle 34489 tendoid 35079 tendo0plr 35098 tendoipl2 35104 erngmul 35112 erngmul-rN 35120 dvamulr 35318 dvavadd 35321 dvhmulr 35393 cdlemm10N 35425 pellfund14 36480 mendmulr 36777 fmuldfeq 38650 stoweidlem19 38912 stoweidlem26 38919 pfxpfxid 40279 pfxcctswrd 40280 0uhgrrusgr 40778 frgruhgr0v 41435 lincval1 42002 |
Copyright terms: Public domain | W3C validator |