Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 598. (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  211  nanass  1512  triun  5220  mapfvd  8821  undifixp  8876  rankpwi  9739  rankelb  9740  2cshwcshw  14752  incexclem  15763  sumeven  16318  cygth  21530  cnpco  23215  txkgen  23600  reperflem  24767  lhop1lem  25978  ulmss  26366  2sqreultblem  27419  crctcshwlkn0lem4  29869  numclwwlk1lem2f1  30415  ontgval  36606  bj-dvelimdv1  37028  eel12131  44989  et-sqrtnegnre  47153  2ffzoeq  47609  iccpartgt  47709  bgoldbtbndlem3  48089  gpgprismgr4cycllem7  48383  lincresunit3  48763