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  213  nanass  1499  triun  5177  mapfvd  8437  undifixp  8492  rankpwi  9246  rankelb  9247  2cshwcshw  14181  incexclem  15185  sumeven  15732  cygth  20712  cnpco  21869  txkgen  22254  reperflem  23420  lhop1lem  24604  ulmss  24979  2sqreultblem  26018  crctcshwlkn0lem4  27585  numclwwlk1lem2f1  28130  ontgval  33774  bj-dvelimdv1  34171  eel12131  41040  2ffzoeq  43522  iccpartgt  43581  bgoldbtbndlem3  43966  lincresunit3  44530