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

Theorem syl221anc 1196
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
sylXanc.5  |-  ( ph  ->  et )
syl221anc.6  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta )  /\  et )  ->  ze )
Assertion
Ref Expression
syl221anc  |-  ( ph  ->  ze )

Proof of Theorem syl221anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
53, 4jca 520 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 sylXanc.5 . 2  |-  ( ph  ->  et )
7 syl221anc.6 . 2  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta )  /\  et )  ->  ze )
81, 2, 5, 6, 7syl211anc 1191 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  syl222anc  1201  vtocldf  3005  f1oprswap  5719  riotasv2dOLD  6597  dmdcand  9821  modmul12d  11282  modnegd  11283  modadd12d  11284  exprec  11423  splval2  11788  eulerthlem2  13173  fermltl  13175  odzdvds  13183  efgredleme  15377  efgredlemc  15379  blssps  18456  blss  18457  metequiv2  18542  met1stc  18553  met2ndci  18554  metdstri  18883  xlebnum  18992  caubl  19262  divcxp  20580  cxple2a  20592  cxplead  20614  cxplt2d  20619  cxple2d  20620  mulcxpd  20621  ang180  20658  wilthlem2  20854  lgslem4  21085  lgsvalmod  21101  lgsmod  21107  lgsdir2lem4  21112  lgsdirprm  21115  lgsne0  21119  lgseisen  21139  xrsmulgzz  24202  ax5seglem9  25878  heiborlem8  26529  pellexlem6  26899  rpexpmord  27013  acongeq  27050  jm2.25  27072  stoweidlem42  27769  stoweidlem51  27778  cdlemd4  31060  cdleme15a  31133  cdleme17b  31146  cdleme25a  31212  cdleme25c  31214  cdleme25dN  31215  cdleme26ee  31219  tendococl  31631  tendodi1  31643  tendodi2  31644  cdlemi  31679  tendocan  31683  cdlemk5a  31694  cdlemk5  31695  cdlemk10  31702  cdlemk5u  31720  cdlemkfid1N  31780
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator