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  1510  triun  5229  mapfvd  8852  undifixp  8907  rankpwi  9776  rankelb  9777  2cshwcshw  14791  incexclem  15802  sumeven  16357  cygth  21481  cnpco  23154  txkgen  23539  reperflem  24707  lhop1lem  25918  ulmss  26306  2sqreultblem  27359  crctcshwlkn0lem4  29743  numclwwlk1lem2f1  30286  ontgval  36419  bj-dvelimdv1  36840  eel12131  44702  et-sqrtnegnre  46871  2ffzoeq  47328  iccpartgt  47428  bgoldbtbndlem3  47808  gpgprismgr4cycllem7  48091  lincresunit3  48470