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  5221  mapfvd  8829  undifixp  8884  rankpwi  9747  rankelb  9748  2cshwcshw  14760  incexclem  15771  sumeven  16326  cygth  21538  cnpco  23223  txkgen  23608  reperflem  24775  lhop1lem  25986  ulmss  26374  2sqreultblem  27427  crctcshwlkn0lem4  29898  numclwwlk1lem2f1  30444  ontgval  36644  bj-dvelimdv1  37091  eel12131  45057  et-sqrtnegnre  47220  2ffzoeq  47676  iccpartgt  47776  bgoldbtbndlem3  48156  gpgprismgr4cycllem7  48450  lincresunit3  48830