Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 597. (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  1510  triun  5274  mapfvd  8919  undifixp  8974  rankpwi  9863  rankelb  9864  2cshwcshw  14864  incexclem  15872  sumeven  16424  cygth  21590  cnpco  23275  txkgen  23660  reperflem  24840  lhop1lem  26052  ulmss  26440  2sqreultblem  27492  crctcshwlkn0lem4  29833  numclwwlk1lem2f1  30376  ontgval  36432  bj-dvelimdv1  36853  eel12131  44733  et-sqrtnegnre  46888  2ffzoeq  47339  iccpartgt  47414  bgoldbtbndlem3  47794  lincresunit3  48398