![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpisyl | Structured version Visualization version GIF version |
Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.) |
Ref | Expression |
---|---|
mpisyl.1 | ⊢ (𝜑 → 𝜓) |
mpisyl.2 | ⊢ 𝜒 |
mpisyl.3 | ⊢ (𝜓 → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
mpisyl | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpisyl.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | mpisyl.2 | . . 3 ⊢ 𝜒 | |
3 | mpisyl.3 | . . 3 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
4 | 2, 3 | mpi 20 | . 2 ⊢ (𝜓 → 𝜃) |
5 | 1, 4 | syl 17 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: ceqsexOLD 3513 ceqsexvOLD 3515 moeq3 3704 fvsng 7189 fveqf1o 7311 fliftcnv 7318 fliftfun 7319 frxp3 8156 orderseqlem 8162 cnvct 9059 undomOLD 9085 pwdom 9154 php 9235 onomeneqOLD 9254 pwfilemOLD 9372 ordiso 9541 ordtypelem8 9550 wdompwdom 9603 unxpwdom 9614 harwdom 9616 inf0 9646 infeq5i 9661 cantnfcl 9692 cardiun 10007 infxpenlem 10038 dfac8b 10056 acnnum 10077 inffien 10088 dfac12lem2 10169 djudoml 10209 cdainflem 10212 djuinf 10213 infunabs 10232 infdju 10233 infdif 10234 infdif2 10235 infmap2 10243 fictb 10270 cofsmo 10294 fin23lem21 10364 hsmexlem1 10451 dmct 10549 mptct 10563 iundomg 10566 iunctb 10599 fpwwe2lem8 10663 canthnum 10674 winalim2 10721 rankcf 10802 tskuni 10808 npomex 11021 hashun2 14378 swrd2lsw 14939 2swrd2eqwrdeq 14940 limsupgord 15452 summolem2 15698 zsum 15700 prodmolem2 15915 zprod 15917 ltoddhalfle 16341 isinv 17746 invsym2 17749 invfun 17750 oppcsect2 17765 oppcinv 17766 efgcpbllemb 19722 frgpuplem 19739 gsumval3 19874 1stcfb 23393 1stcrestlem 23400 2ndcdisj2 23405 txdis1cn 23583 tx1stc 23598 tgphaus 24065 qustgplem 24069 tsmsxp 24103 xmeter 24383 bndth 24928 clmneg1 25053 ovolctb2 25465 ovoliunlem1 25475 i1fd 25654 dvgt0lem2 25980 taylf 26340 efcvx 26431 logccv 26642 loglesqrt 26738 0elold 27881 noseqrdgfn 28229 usgredg2v 29112 crctcshtrl 29706 frgr3vlem1 30155 strlem6 32138 mptctf 32581 omsmeas 34074 sibfof 34091 bnj97 34628 bnj553 34660 bnj966 34706 bnj1442 34811 subfaclefac 34917 erdsze2lem1 34944 erdsze2lem2 34945 snmlff 35070 satffunlem2lem2 35147 bj-ssbid2ALT 36270 phpreu 37208 ptrecube 37224 poimirlem3 37227 poimirlem32 37256 heicant 37259 dvhopellsm 40720 pell1qrgaplem 42435 dnwech 42614 oaun3lem1 42945 mnurndlem1 43860 rn1st 44788 stoweid 45589 dirkercncflem2 45630 fourierdlem36 45669 |
Copyright terms: Public domain | W3C validator |