![]() |
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 594. (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 2236 ax13ALT 2418 r19.30 3109 intss2 5112 vtoclr 5741 funopg 6588 feldmfvelcdm 7095 abnex 7760 xpider 8807 undifixp 8953 onsdominel 9154 fodomr 9156 wemaplem2 9577 rankuni2b 9883 infxpenlem 10043 dfac8b 10061 ac10ct 10064 alephordi 10104 infdif 10239 cfflb 10289 alephval2 10602 tskxpss 10802 tskcard 10811 ingru 10845 grur1 10850 grothac 10860 suplem1pr 11082 mulgt0sr 11135 ixxssixx 13378 difelfzle 13654 swrdnd0 14651 climrlim2 15535 qshash 15817 gcdcllem3 16487 vdwlem13 16981 ocvsscon 21641 opsrtoslem2 22039 txcnp 23585 t0kq 23783 filconn 23848 filuni 23850 alexsubALTlem3 24014 rectbntr0 24809 iscau4 25268 cfilres 25285 lmcau 25302 bcthlem2 25314 subfacp1lem6 34946 cvmsdisj 35031 meran1 36046 bj-bi3ant 36217 bj-cbv3ta 36414 bj-2upleq 36642 bj-ismooredr2 36740 bj-snmoore 36743 bj-isclm 36921 relowlssretop 36993 poimirlem30 37274 poimirlem31 37275 caushft 37385 partimeq 38431 ax13fromc9 38528 harinf 42602 ntrk0kbimka 43616 onfrALTlem3 44130 onfrALTlem2 44132 e222 44222 e111 44260 e333 44319 bitr3VD 44435 disjinfi 44709 prpair 46983 onsetrec 48330 aacllem 48425 |
Copyright terms: Public domain | W3C validator |