Theorem syl2imc 42

Description: A commuted version of syl2im 41. Implication-only version of syl2anr 609. (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 41	. 2 ⊢ (𝜑 → (𝜒 → 𝜏))
5	4	com12 33	1 ⊢ (𝜒 → (𝜑 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  impbid21d  214  nanass  1540  triun  5226  imadifssran  6191  mapfvd  8885  undifixp  8940  rankpwi  9805  rankelb  9806  2cshwcshw  14944  incexclem  15973  sumeven  16525  sumodd  16526  cygth  21839  cnpco  23547  txkgen  23933  reperflem  25100  lhop1lem  26295  ulmss  26688  2sqreultblem  27739  crctcshwlkn0lem4  30336  numclwwlk1lem2f1  30892  ontgval  37141  bj-dvelimdv1  37686  eel12131  45639  et-sqrtnegnre  47805  2ffzoeq  48320  iccpartgt  48431  bgoldbtbndlem3  48827  gpgprismgr4cycllem7  49121  lincresunit3  49515