Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 605. (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  213  nanass  1524  triun  5216  mapfvd  8850  undifixp  8905  rankpwi  9771  rankelb  9772  2cshwcshw  14828  incexclem  15842  sumeven  16397  cygth  21596  cnpco  23300  txkgen  23685  reperflem  24852  lhop1lem  26048  ulmss  26430  2sqreultblem  27482  crctcshwlkn0lem4  29952  numclwwlk1lem2f1  30498  ontgval  36739  bj-dvelimdv1  37285  eel12131  45236  et-sqrtnegnre  47395  2ffzoeq  47870  iccpartgt  47981  bgoldbtbndlem3  48377  gpgprismgr4cycllem7  48671  lincresunit3  49051