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  5208  mapfvd  8827  undifixp  8882  rankpwi  9747  rankelb  9748  2cshwcshw  14787  incexclem  15801  sumeven  16356  cygth  21551  cnpco  23232  txkgen  23617  reperflem  24784  lhop1lem  25980  ulmss  26362  2sqreultblem  27411  crctcshwlkn0lem4  29881  numclwwlk1lem2f1  30427  ontgval  36613  bj-dvelimdv1  37159  eel12131  45139  et-sqrtnegnre  47301  2ffzoeq  47770  iccpartgt  47881  bgoldbtbndlem3  48277  gpgprismgr4cycllem7  48571  lincresunit3  48951