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  211  nanass  1510  triun  5244  mapfvd  8893  undifixp  8948  rankpwi  9837  rankelb  9838  2cshwcshw  14844  incexclem  15852  sumeven  16406  cygth  21532  cnpco  23205  txkgen  23590  reperflem  24758  lhop1lem  25970  ulmss  26358  2sqreultblem  27411  crctcshwlkn0lem4  29795  numclwwlk1lem2f1  30338  ontgval  36449  bj-dvelimdv1  36870  eel12131  44737  et-sqrtnegnre  46902  2ffzoeq  47356  iccpartgt  47441  bgoldbtbndlem3  47821  gpgprismgr4cycllem7  48100  lincresunit3  48457