Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 598. (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  1512  triun  5207  mapfvd  8820  undifixp  8875  rankpwi  9738  rankelb  9739  2cshwcshw  14778  incexclem  15792  sumeven  16347  cygth  21561  cnpco  23242  txkgen  23627  reperflem  24794  lhop1lem  25990  ulmss  26375  2sqreultblem  27425  crctcshwlkn0lem4  29896  numclwwlk1lem2f1  30442  ontgval  36629  bj-dvelimdv1  37175  eel12131  45157  et-sqrtnegnre  47319  2ffzoeq  47788  iccpartgt  47899  bgoldbtbndlem3  48295  gpgprismgr4cycllem7  48589  lincresunit3  48969