| 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 596. (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 2249 ax13ALT 2430 r19.30 3120 intss2 5108 vtoclr 5748 funopg 6600 feldmfvelcdm 7106 abnex 7777 xpider 8828 undifixp 8974 onsdominel 9166 fodomr 9168 fodomfir 9368 wemaplem2 9587 rankuni2b 9893 infxpenlem 10053 dfac8b 10071 ac10ct 10074 alephordi 10114 infdif 10248 cfflb 10299 alephval2 10612 tskxpss 10812 tskcard 10821 ingru 10855 grur1 10860 grothac 10870 suplem1pr 11092 mulgt0sr 11145 ixxssixx 13401 difelfzle 13681 swrdnd0 14695 climrlim2 15583 qshash 15863 gcdcllem3 16538 vdwlem13 17031 ocvsscon 21693 opsrtoslem2 22080 txcnp 23628 t0kq 23826 filconn 23891 filuni 23893 alexsubALTlem3 24057 rectbntr0 24854 iscau4 25313 cfilres 25330 lmcau 25347 bcthlem2 25359 subfacp1lem6 35190 cvmsdisj 35275 meran1 36412 bj-bi3ant 36590 bj-cbv3ta 36787 bj-2upleq 37013 bj-ismooredr2 37111 bj-snmoore 37114 bj-isclm 37292 relowlssretop 37364 poimirlem30 37657 poimirlem31 37658 caushft 37768 partimeq 38810 ax13fromc9 38907 harinf 43046 ntrk0kbimka 44052 onfrALTlem3 44564 onfrALTlem2 44566 e222 44656 e111 44694 e333 44753 bitr3VD 44869 disjinfi 45197 prpair 47488 onsetrec 49227 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |