![]() |
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 595. (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 2237 ax13ALT 2420 r19.30 3116 intss2 5105 vtoclr 5735 funopg 6581 feldmfvelcdm 7090 abnex 7753 xpider 8800 undifixp 8946 onsdominel 9144 fodomr 9146 wemaplem2 9564 rankuni2b 9870 infxpenlem 10030 dfac8b 10048 ac10ct 10051 alephordi 10091 infdif 10226 cfflb 10276 alephval2 10589 tskxpss 10789 tskcard 10798 ingru 10832 grur1 10837 grothac 10847 suplem1pr 11069 mulgt0sr 11122 ixxssixx 13364 difelfzle 13640 swrdnd0 14633 climrlim2 15517 qshash 15799 gcdcllem3 16469 vdwlem13 16955 ocvsscon 21600 opsrtoslem2 21993 txcnp 23517 t0kq 23715 filconn 23780 filuni 23782 alexsubALTlem3 23946 rectbntr0 24741 iscau4 25200 cfilres 25217 lmcau 25234 bcthlem2 25246 subfacp1lem6 34789 cvmsdisj 34874 meran1 35889 bj-bi3ant 36060 bj-cbv3ta 36257 bj-2upleq 36485 bj-ismooredr2 36583 bj-snmoore 36586 bj-isclm 36764 relowlssretop 36836 poimirlem30 37117 poimirlem31 37118 caushft 37228 partimeq 38275 ax13fromc9 38372 harinf 42449 ntrk0kbimka 43463 onfrALTlem3 43977 onfrALTlem2 43979 e222 44069 e111 44107 e333 44166 bitr3VD 44282 disjinfi 44559 prpair 46835 onsetrec 48133 aacllem 48228 |
Copyright terms: Public domain | W3C validator |