Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 603. (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  212  nanass  1517  triun  5201  mapfvd  8824  undifixp  8879  rankpwi  9745  rankelb  9746  2cshwcshw  14785  incexclem  15799  sumeven  16354  cygth  21553  cnpco  23257  txkgen  23642  reperflem  24809  lhop1lem  26005  ulmss  26387  2sqreultblem  27436  crctcshwlkn0lem4  29906  numclwwlk1lem2f1  30452  ontgval  36660  bj-dvelimdv1  37206  eel12131  45157  et-sqrtnegnre  47317  2ffzoeq  47792  iccpartgt  47903  bgoldbtbndlem3  48299  gpgprismgr4cycllem7  48593  lincresunit3  48973