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  1507  triun  5280  mapfvd  8918  undifixp  8973  rankpwi  9861  rankelb  9862  2cshwcshw  14861  incexclem  15869  sumeven  16421  cygth  21608  cnpco  23291  txkgen  23676  reperflem  24854  lhop1lem  26067  ulmss  26455  2sqreultblem  27507  crctcshwlkn0lem4  29843  numclwwlk1lem2f1  30386  ontgval  36414  bj-dvelimdv1  36835  eel12131  44711  et-sqrtnegnre  46829  2ffzoeq  47277  iccpartgt  47352  bgoldbtbndlem3  47732  lincresunit3  48327