Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 597. (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  1508  triun  5280  mapfvd  8872  undifixp  8927  rankpwi  9817  rankelb  9818  2cshwcshw  14775  incexclem  15781  sumeven  16329  cygth  21126  cnpco  22770  txkgen  23155  reperflem  24333  lhop1lem  25529  ulmss  25908  2sqreultblem  26948  crctcshwlkn0lem4  29064  numclwwlk1lem2f1  29607  ontgval  35311  bj-dvelimdv1  35726  eel12131  43464  et-sqrtnegnre  45579  2ffzoeq  46026  iccpartgt  46085  bgoldbtbndlem3  46465  lincresunit3  47152