Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 596. (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  210  nanass  1502  triun  5200  mapfvd  8625  undifixp  8680  rankpwi  9512  rankelb  9513  2cshwcshw  14466  incexclem  15476  sumeven  16024  cygth  20691  cnpco  22326  txkgen  22711  reperflem  23887  lhop1lem  25082  ulmss  25461  2sqreultblem  26501  crctcshwlkn0lem4  28079  numclwwlk1lem2f1  28622  ontgval  34547  bj-dvelimdv1  34963  eel12131  42222  2ffzoeq  44708  iccpartgt  44767  bgoldbtbndlem3  45147  lincresunit3  45710