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

Theorem syl6c 64
Description: Inference combining syl6 33 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 33 . 2
51, 4mpdd 40 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  syl6ci  65  syldd  66  impbidd  189  pm5.21ndd  354  jcad  533  zorn2lem6  8902  sqreulem  13192  ontopbas  29893  ontgval  29896  ordtoplem  29900  ordcmp  29912  ee33  33291  sb5ALT  33295  tratrb  33307  onfrALTlem2  33318  onfrALT  33321  ax6e2ndeq  33332  ee22an  33459  sspwtrALT  33620  sspwtrALT2  33623  trintALT  33681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator