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

Theorem syl6c 70
 Description: Inference combining syl6 35 with contraction. (Contributed by Alan Sare, 2-May-2011.)
Hypotheses
Ref Expression
syl6c.1 (𝜑 → (𝜓𝜒))
syl6c.2 (𝜑 → (𝜓𝜃))
syl6c.3 (𝜒 → (𝜃𝜏))
Assertion
Ref Expression
syl6c (𝜑 → (𝜓𝜏))

Proof of Theorem syl6c
StepHypRef Expression
1 syl6c.2 . 2 (𝜑 → (𝜓𝜃))
2 syl6c.1 . . 3 (𝜑 → (𝜓𝜒))
3 syl6c.3 . . 3 (𝜒 → (𝜃𝜏))
42, 3syl6 35 . 2 (𝜑 → (𝜓 → (𝜃𝜏)))
51, 4mpdd 43 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:  syl6ci  71  syldd  72  impbidd  212  pm5.21ndd  383  jcad  515  a2and  841  zorn2lem6  9901  sqreulem  14699  ontopbas  33784  ontgval  33787  ordtoplem  33791  ordcmp  33803  fvineqsneu  34709  jaodd  39212  ee33  41010  sb5ALT  41014  tratrb  41025  onfrALTlem2  41035  onfrALT  41038  ax6e2ndeq  41048  ee22an  41162  sspwtrALT  41311  sspwtrALT2  41312  trintALT  41370
 Copyright terms: Public domain W3C validator