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  5236  mapfvd  8751  undifixp  8806  rankpwi  9693  rankelb  9694  2cshwcshw  14647  incexclem  15657  sumeven  16205  cygth  20907  cnpco  22546  txkgen  22931  reperflem  24109  lhop1lem  25305  ulmss  25684  2sqreultblem  26724  crctcshwlkn0lem4  28563  numclwwlk1lem2f1  29106  ontgval  34834  bj-dvelimdv1  35249  eel12131  42796  et-sqrtnegnre  44905  2ffzoeq  45351  iccpartgt  45410  bgoldbtbndlem3  45790  lincresunit3  46353
  Copyright terms: Public domain W3C validator