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 14212 swrd2lsw 14774 2swrd2eqwrdeq 14775 limsupgord 15290 summolem2 15537 zsum 15539 prodmolem2 15754 zprod 15756 ltoddhalfle 16179 isinv 17579 invsym2 17582 invfun 17583 oppcsect2 17598 oppcinv 17599 efgcpbllemb 19472 frgpuplem 19489 gsumval3 19619 1stcfb 22724 1stcrestlem 22731 2ndcdisj2 22736 txdis1cn 22914 tx1stc 22929 tgphaus 23396 qustgplem 23400 tsmsxp 23434 xmeter 23714 bndth 24249 clmneg1 24373 ovolctb2 24784 ovoliunlem1 24794 i1fd 24973 dvgt0lem2 25295 taylf 25648 efcvx 25736 logccv 25946 loglesqrt 26039 usgredg2v 27980 crctcshtrl 28573 frgr3vlem1 29022 strlem6 31003 mptctf 31435 omsmeas 32703 sibfof 32720 bnj97 33258 bnj553 33290 bnj966 33336 bnj1442 33441 subfaclefac 33550 erdsze2lem1 33577 erdsze2lem2 33578 snmlff 33703 satffunlem2lem2 33780 frxp3 34189 bj-ssbid2ALT 35058 phpreu 35993 ptrecube 36009 poimirlem3 36012 poimirlem32 36041 heicant 36044 dvhopellsm 39511 pell1qrgaplem 41098 dnwech 41277 mnurndlem1 42362 rn1st 43298 stoweid 44095 dirkercncflem2 44136 fourierdlem36 44175 |
Copyright terms: Public domain | W3C validator |