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  5231  imadifssran  6201  mapfvd  8889  undifixp  8944  rankpwi  9808  rankelb  9809  2cshwcshw  14898  incexclem  15927  sumeven  16481  sumodd  16482  cygth  21788  cnpco  23496  txkgen  23882  reperflem  25049  lhop1lem  26245  ulmss  26633  2sqreultblem  27685  crctcshwlkn0lem4  30282  numclwwlk1lem2f1  30838  ontgval  37052  bj-dvelimdv1  37597  eel12131  45537  et-sqrtnegnre  47703  2ffzoeq  48218  iccpartgt  48329  bgoldbtbndlem3  48725  gpgprismgr4cycllem7  49019  lincresunit3  49413