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  5232  mapfvd  8855  undifixp  8910  rankpwi  9783  rankelb  9784  2cshwcshw  14798  incexclem  15809  sumeven  16364  cygth  21488  cnpco  23161  txkgen  23546  reperflem  24714  lhop1lem  25925  ulmss  26313  2sqreultblem  27366  crctcshwlkn0lem4  29750  numclwwlk1lem2f1  30293  ontgval  36426  bj-dvelimdv1  36847  eel12131  44709  et-sqrtnegnre  46878  2ffzoeq  47332  iccpartgt  47432  bgoldbtbndlem3  47812  gpgprismgr4cycllem7  48095  lincresunit3  48474