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  1511  triun  5210  mapfvd  8798  undifixp  8853  rankpwi  9708  rankelb  9709  2cshwcshw  14724  incexclem  15735  sumeven  16290  cygth  21501  cnpco  23175  txkgen  23560  reperflem  24727  lhop1lem  25938  ulmss  26326  2sqreultblem  27379  crctcshwlkn0lem4  29784  numclwwlk1lem2f1  30327  ontgval  36444  bj-dvelimdv1  36865  eel12131  44724  et-sqrtnegnre  46890  2ffzoeq  47337  iccpartgt  47437  bgoldbtbndlem3  47817  gpgprismgr4cycllem7  48111  lincresunit3  48492