Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 599. (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  214  nanass  1501  triun  5149  mapfvd  8426  undifixp  8481  rankpwi  9236  rankelb  9237  2cshwcshw  14178  incexclem  15183  sumeven  15728  cygth  20263  cnpco  21872  txkgen  22257  reperflem  23423  lhop1lem  24616  ulmss  24992  2sqreultblem  26032  crctcshwlkn0lem4  27599  numclwwlk1lem2f1  28142  ontgval  33892  bj-dvelimdv1  34291  eel12131  41419  2ffzoeq  43885  iccpartgt  43944  bgoldbtbndlem3  44325  lincresunit3  44890