Theorem syl2imc 42

Description: A commuted version of syl2im 41. Implication-only version of syl2anr 608. (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  triun  5232  imadifssran  6201  mapfvd  8875  undifixp  8930  rankpwi  9793  rankelb  9794  2cshwcshw  14869  incexclem  15897  sumeven  16451  cygth  21732  cnpco  23435  txkgen  23820  reperflem  24987  lhop1lem  26183  ulmss  26571  2sqreultblem  27623  crctcshwlkn0lem4  30173  numclwwlk1lem2f1  30719  ontgval  36970  bj-dvelimdv1  37515  eel12131  45449  et-sqrtnegnre  47615  2ffzoeq  48093  iccpartgt  48204  bgoldbtbndlem3  48600  gpgprismgr4cycllem7  48894  lincresunit3  49289