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  211  pm5.21ndd  381  jcad  513  a2and  839  zorn2lem6  9911  sqreulem  14707  ontopbas  33673  ontgval  33676  ordtoplem  33680  ordcmp  33692  fvineqsneu  34574  jaodd  38979  ee33  40732  sb5ALT  40736  tratrb  40747  onfrALTlem2  40757  onfrALT  40760  ax6e2ndeq  40770  ee22an  40884  sspwtrALT  41033  sspwtrALT2  41034  trintALT  41092
  Copyright terms: Public domain W3C validator