![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl2im | Structured version Visualization version GIF version |
Description: Replace two antecedents. Implication-only version of syl2an 597. (Contributed by Wolf Lammen, 14-May-2013.) |
Ref | Expression |
---|---|
syl2im.1 | ⊢ (𝜑 → 𝜓) |
syl2im.2 | ⊢ (𝜒 → 𝜃) |
syl2im.3 | ⊢ (𝜓 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
syl2im | ⊢ (𝜑 → (𝜒 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2im.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl2im.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
3 | syl2im.3 | . . 3 ⊢ (𝜓 → (𝜃 → 𝜏)) | |
4 | 2, 3 | syl5 34 | . 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: syl2imc 41 sylc 65 sbequ2 2242 ax13ALT 2424 r19.30 3120 intss2 5072 vtoclr 5699 funopg 6539 abnex 7695 xpider 8733 undifixp 8878 onsdominel 9076 fodomr 9078 wemaplem2 9491 rankuni2b 9797 infxpenlem 9957 dfac8b 9975 ac10ct 9978 alephordi 10018 infdif 10153 cfflb 10203 alephval2 10516 tskxpss 10716 tskcard 10725 ingru 10759 grur1 10764 grothac 10774 suplem1pr 10996 mulgt0sr 11049 ixxssixx 13287 difelfzle 13563 swrdnd0 14554 climrlim2 15438 qshash 15720 gcdcllem3 16389 vdwlem13 16873 ocvsscon 21102 opsrtoslem2 21486 txcnp 22994 t0kq 23192 filconn 23257 filuni 23259 alexsubALTlem3 23423 rectbntr0 24218 iscau4 24666 cfilres 24683 lmcau 24700 bcthlem2 24712 subfacp1lem6 33843 cvmsdisj 33928 meran1 34936 bj-bi3ant 35107 bj-cbv3ta 35304 bj-2upleq 35533 bj-ismooredr2 35631 bj-snmoore 35634 bj-isclm 35812 relowlssretop 35884 poimirlem30 36158 poimirlem31 36159 caushft 36270 partimeq 37321 ax13fromc9 37418 harinf 41405 ntrk0kbimka 42403 onfrALTlem3 42918 onfrALTlem2 42920 e222 43010 e111 43048 e333 43107 bitr3VD 43223 disjinfi 43504 prpair 45783 onsetrec 47243 aacllem 47338 |
Copyright terms: Public domain | W3C validator |