MPE Home 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  210  pm5.21ndd  379  jcad  512  a2and  845  zorn2lem6  10539  sqreulem  15395  ontopbas  36411  ontgval  36414  ordtoplem  36418  ordcmp  36430  fvineqsneu  37394  jaodd  42227  ee33  44519  sb5ALT  44523  tratrb  44534  onfrALTlem2  44544  onfrALT  44547  ax6e2ndeq  44557  ee22an  44671  sspwtrALT  44820  sspwtrALT2  44821  trintALT  44879
  Copyright terms: Public domain W3C validator