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  5216  mapfvd  8813  undifixp  8868  rankpwi  9738  rankelb  9739  2cshwcshw  14750  incexclem  15761  sumeven  16316  cygth  21496  cnpco  23170  txkgen  23555  reperflem  24723  lhop1lem  25934  ulmss  26322  2sqreultblem  27375  crctcshwlkn0lem4  29776  numclwwlk1lem2f1  30319  ontgval  36404  bj-dvelimdv1  36825  eel12131  44686  et-sqrtnegnre  46855  2ffzoeq  47312  iccpartgt  47412  bgoldbtbndlem3  47792  gpgprismgr4cycllem7  48075  lincresunit3  48454