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  210  nanass  1505  triun  5204  mapfvd  8667  undifixp  8722  rankpwi  9581  rankelb  9582  2cshwcshw  14538  incexclem  15548  sumeven  16096  cygth  20779  cnpco  22418  txkgen  22803  reperflem  23981  lhop1lem  25177  ulmss  25556  2sqreultblem  26596  crctcshwlkn0lem4  28178  numclwwlk1lem2f1  28721  ontgval  34620  bj-dvelimdv1  35036  eel12131  42333  2ffzoeq  44820  iccpartgt  44879  bgoldbtbndlem3  45259  lincresunit3  45822