Theorem syl2imc 42

Description: A commuted version of syl2im 41. Implication-only version of syl2anr 608. (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 41	. 2 ⊢ (𝜑 → (𝜒 → 𝜏))
5	4	com12 33	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  214  nanass  1533  triun  5227  mapfvd  8865  undifixp  8920  rankpwi  9783  rankelb  9784  2cshwcshw  14852  incexclem  15880  sumeven  16435  cygth  21681  cnpco  23385  txkgen  23770  reperflem  24937  lhop1lem  26133  ulmss  26518  2sqreultblem  27570  crctcshwlkn0lem4  30071  numclwwlk1lem2f1  30617  ontgval  36804  bj-dvelimdv1  37349  eel12131  45286  et-sqrtnegnre  47445  2ffzoeq  47920  iccpartgt  48031  bgoldbtbndlem3  48427  gpgprismgr4cycllem7  48721  lincresunit3  49112