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  ax12ev2c  2220  triun  5230  imadifssranOLD  6215  mapfvd  8935  undifixp  8990  rankpwi  9859  rankelb  9860  2cshwcshw  15004  incexclem  16034  sumeven  16586  sumodd  16587  cygth  21907  cnpco  23615  txkgen  24001  reperflem  25168  lhop1lem  26363  ulmss  26754  2sqreultblem  27805  crctcshwlkn0lem4  30432  numclwwlk1lem2f1  30988  ontgval  37397  bj-dvelimdv1  37942  eel12131  45886  et-sqrtnegnre  48088  2ffzoeq  48603  iccpartgt  48714  bgoldbtbndlem3  49110  gpgprismgr4cycllem7  49404  lincresunit3  49798