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  8818  undifixp  8873  rankpwi  9736  rankelb  9737  2cshwcshw  14776  incexclem  15790  sumeven  16345  cygth  21559  cnpco  23241  txkgen  23626  reperflem  24793  lhop1lem  25990  ulmss  26377  2sqreultblem  27430  crctcshwlkn0lem4  29901  numclwwlk1lem2f1  30447  ontgval  36634  bj-dvelimdv1  37172  eel12131  45154  et-sqrtnegnre  47316  2ffzoeq  47773  iccpartgt  47884  bgoldbtbndlem3  48280  gpgprismgr4cycllem7  48574  lincresunit3  48954