Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 595. (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 40	. 2 ⊢ (𝜑 → (𝜒 → 𝜏))
5	4	com12 32	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  210  nanass  1506  triun  5279  mapfvd  8875  undifixp  8930  rankpwi  9820  rankelb  9821  2cshwcshw  14780  incexclem  15786  sumeven  16334  cygth  21346  cnpco  22991  txkgen  23376  reperflem  24554  lhop1lem  25765  ulmss  26145  2sqreultblem  27187  crctcshwlkn0lem4  29334  numclwwlk1lem2f1  29877  ontgval  35619  bj-dvelimdv1  36034  eel12131  43776  et-sqrtnegnre  45887  2ffzoeq  46334  iccpartgt  46393  bgoldbtbndlem3  46773  lincresunit3  47249