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  213  nanass  1496  triun  5176  mapfvd  8435  undifixp  8490  rankpwi  9244  rankelb  9245  2cshwcshw  14179  incexclem  15183  sumeven  15730  cygth  20710  cnpco  21867  txkgen  22252  reperflem  23418  lhop1lem  24602  ulmss  24977  2sqreultblem  26016  crctcshwlkn0lem4  27583  numclwwlk1lem2f1  28128  ontgval  33772  bj-dvelimdv1  34169  eel12131  41037  2ffzoeq  43518  iccpartgt  43577  bgoldbtbndlem3  43962  lincresunit3  44526
  Copyright terms: Public domain W3C validator