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  1539  ax12ev2c  2216  triun  5226  imadifssranOLD  6202  mapfvd  8908  undifixp  8963  rankpwi  9833  rankelb  9834  2cshwcshw  14977  incexclem  16006  sumeven  16558  sumodd  16559  cygth  21878  cnpco  23586  txkgen  23972  reperflem  25139  lhop1lem  26334  ulmss  26725  2sqreultblem  27776  crctcshwlkn0lem4  30403  numclwwlk1lem2f1  30959  ontgval  37294  bj-dvelimdv1  37839  eel12131  45771  et-sqrtnegnre  47959  2ffzoeq  48474  iccpartgt  48585  bgoldbtbndlem3  48981  gpgprismgr4cycllem7  49275  lincresunit3  49669