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  211  nanass  1507  triun  5298  mapfvd  8937  undifixp  8992  rankpwi  9892  rankelb  9893  2cshwcshw  14874  incexclem  15884  sumeven  16435  cygth  21613  cnpco  23296  txkgen  23681  reperflem  24859  lhop1lem  26072  ulmss  26458  2sqreultblem  27510  crctcshwlkn0lem4  29846  numclwwlk1lem2f1  30389  ontgval  36397  bj-dvelimdv1  36818  eel12131  44684  et-sqrtnegnre  46794  2ffzoeq  47242  iccpartgt  47301  bgoldbtbndlem3  47681  lincresunit3  48210