Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 595. (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  210  nanass  1504  triun  5286  mapfvd  8912  undifixp  8967  rankpwi  9867  rankelb  9868  2cshwcshw  14847  incexclem  15853  sumeven  16402  cygth  21581  cnpco  23262  txkgen  23647  reperflem  24825  lhop1lem  26037  ulmss  26423  2sqreultblem  27474  crctcshwlkn0lem4  29789  numclwwlk1lem2f1  30332  ontgval  36229  bj-dvelimdv1  36643  eel12131  44501  et-sqrtnegnre  46605  2ffzoeq  47051  iccpartgt  47110  bgoldbtbndlem3  47490  lincresunit3  47986