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  1511  triun  5216  mapfvd  8812  undifixp  8867  rankpwi  9726  rankelb  9727  2cshwcshw  14742  incexclem  15753  sumeven  16308  cygth  21518  cnpco  23192  txkgen  23577  reperflem  24744  lhop1lem  25955  ulmss  26343  2sqreultblem  27396  crctcshwlkn0lem4  29802  numclwwlk1lem2f1  30348  ontgval  36486  bj-dvelimdv1  36907  eel12131  44819  et-sqrtnegnre  46985  2ffzoeq  47441  iccpartgt  47541  bgoldbtbndlem3  47921  gpgprismgr4cycllem7  48215  lincresunit3  48596