Theorem syl2imc 42

Description: A commuted version of syl2im 41. Implication-only version of syl2anr 608. (Contributed by BJ, 20-Oct-2021.)

Hypotheses

Ref	Expression
syl2im.1	⊢ (𝜑 → 𝜓)
syl2im.2	⊢ (𝜒 → 𝜃)
syl2im.3	⊢ (𝜓 → (𝜃 → 𝜏))

Assertion

Ref	Expression
syl2imc	⊢ (𝜒 → (𝜑 → 𝜏))

Proof of Theorem syl2imc

Step	Hyp	Ref	Expression
1		syl2im.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl2im.2	. . 3 ⊢ (𝜒 → 𝜃)
3		syl2im.3	. . 3 ⊢ (𝜓 → (𝜃 → 𝜏))
4	1, 2, 3	syl2im 41	. 2 ⊢ (𝜑 → (𝜒 → 𝜏))
5	4	com12 33	1 ⊢ (𝜒 → (𝜑 → 𝜏))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  impbid21d  214  nanass  1538  triun  5232  imadifssran  6202  mapfvd  8876  undifixp  8931  rankpwi  9794  rankelb  9795  2cshwcshw  14862  incexclem  15890  sumeven  16444  cygth  21700  cnpco  23403  txkgen  23788  reperflem  24955  lhop1lem  26151  ulmss  26536  2sqreultblem  27588  crctcshwlkn0lem4  30128  numclwwlk1lem2f1  30674  ontgval  36908  bj-dvelimdv1  37453  eel12131  45391  et-sqrtnegnre  47557  2ffzoeq  48032  iccpartgt  48143  bgoldbtbndlem3  48539  gpgprismgr4cycllem7  48833  lincresunit3  49228