MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2imc Structured version   Visualization version   GIF version

Theorem syl2imc 41
Description: A commuted version of syl2im 40. Implication-only version of syl2anr 598. (Contributed by BJ, 20-Oct-2021.)
Hypotheses
Ref Expression
syl2im.1 (𝜑𝜓)
syl2im.2 (𝜒𝜃)
syl2im.3 (𝜓 → (𝜃𝜏))
Assertion
Ref Expression
syl2imc (𝜒 → (𝜑𝜏))

Proof of Theorem syl2imc
StepHypRef Expression
1 syl2im.1 . . 3 (𝜑𝜓)
2 syl2im.2 . . 3 (𝜒𝜃)
3 syl2im.3 . . 3 (𝜓 → (𝜃𝜏))
41, 2, 3syl2im 40 . 2 (𝜑 → (𝜒𝜏))
54com12 32 1 (𝜒 → (𝜑𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  impbid21d  210  nanass  1509  triun  5241  mapfvd  8823  undifixp  8878  rankpwi  9767  rankelb  9768  2cshwcshw  14723  incexclem  15729  sumeven  16277  cygth  21001  cnpco  22641  txkgen  23026  reperflem  24204  lhop1lem  25400  ulmss  25779  2sqreultblem  26819  crctcshwlkn0lem4  28807  numclwwlk1lem2f1  29350  ontgval  34956  bj-dvelimdv1  35371  eel12131  43087  et-sqrtnegnre  45204  2ffzoeq  45650  iccpartgt  45709  bgoldbtbndlem3  46089  lincresunit3  46652
  Copyright terms: Public domain W3C validator