Theorem syl2imc 41

Description: A commuted version of syl2im 40. Implication-only version of syl2anr 600. (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  214  nanass  1502  triun  5149  mapfvd  8459  undifixp  8514  rankpwi  9275  rankelb  9276  2cshwcshw  14224  incexclem  15229  sumeven  15778  cygth  20329  cnpco  21957  txkgen  22342  reperflem  23509  lhop1lem  24702  ulmss  25081  2sqreultblem  26121  crctcshwlkn0lem4  27688  numclwwlk1lem2f1  28231  ontgval  34159  bj-dvelimdv1  34562  eel12131  41782  2ffzoeq  44243  iccpartgt  44302  bgoldbtbndlem3  44682  lincresunit3  45245