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 3492 ceqsexvOLD 3494 moeq3 3669 fvsng 7121 fveqf1o 7244 fliftcnv 7251 fliftfun 7252 orderseqlem 8057 cnvct 8912 undomOLD 8938 pwdom 9007 php 9088 onomeneqOLD 9107 pwfilemOLD 9224 ordiso 9386 ordtypelem8 9395 wdompwdom 9448 unxpwdom 9459 harwdom 9461 inf0 9491 infeq5i 9506 cantnfcl 9537 cardiun 9852 infxpenlem 9883 dfac8b 9901 acnnum 9922 inffien 9933 dfac12lem2 10014 djudoml 10054 cdainflem 10057 djuinf 10058 infunabs 10077 infdju 10078 infdif 10079 infdif2 10080 infmap2 10088 fictb 10115 cofsmo 10139 fin23lem21 10209 hsmexlem1 10296 dmct 10394 mptct 10408 iundomg 10411 iunctb 10444 fpwwe2lem8 10508 canthnum 10519 winalim2 10566 rankcf 10647 tskuni 10653 npomex 10866 hashun2 14211 swrd2lsw 14773 2swrd2eqwrdeq 14774 limsupgord 15289 summolem2 15536 zsum 15538 prodmolem2 15753 zprod 15755 ltoddhalfle 16178 isinv 17578 invsym2 17581 invfun 17582 oppcsect2 17597 oppcinv 17598 efgcpbllemb 19467 frgpuplem 19484 gsumval3 19614 1stcfb 22719 1stcrestlem 22726 2ndcdisj2 22731 txdis1cn 22909 tx1stc 22924 tgphaus 23391 qustgplem 23395 tsmsxp 23429 xmeter 23709 bndth 24244 clmneg1 24368 ovolctb2 24779 ovoliunlem1 24789 i1fd 24968 dvgt0lem2 25290 taylf 25643 efcvx 25731 logccv 25941 loglesqrt 26034 usgredg2v 27974 crctcshtrl 28567 frgr3vlem1 29016 strlem6 30997 mptctf 31429 omsmeas 32697 sibfof 32714 bnj97 33252 bnj553 33284 bnj966 33330 bnj1442 33435 subfaclefac 33544 erdsze2lem1 33571 erdsze2lem2 33572 snmlff 33697 satffunlem2lem2 33774 frxp3 34186 bj-ssbid2ALT 35023 phpreu 35958 ptrecube 35974 poimirlem3 35977 poimirlem32 36006 heicant 36009 dvhopellsm 39476 pell1qrgaplem 41062 dnwech 41241 mnurndlem1 42326 rn1st 43262 stoweid 44059 dirkercncflem2 44100 fourierdlem36 44139 |
Copyright terms: Public domain | W3C validator |