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 600. (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  214  nanass  1502  triun  5149  mapfvd  8459  undifixp  8514  rankpwi  9275  rankelb  9276  2cshwcshw  14224  incexclem  15229  sumeven  15778  cygth  20329  cnpco  21957  txkgen  22342  reperflem  23509  lhop1lem  24702  ulmss  25081  2sqreultblem  26121  crctcshwlkn0lem4  27688  numclwwlk1lem2f1  28231  ontgval  34159  bj-dvelimdv1  34562  eel12131  41782  2ffzoeq  44243  iccpartgt  44302  bgoldbtbndlem3  44682  lincresunit3  45245
 Copyright terms: Public domain W3C validator