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

Theorem syl221anc 1241
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 530 . 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 1236 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 976
This theorem is referenced by:  syl222anc  1246  vtocldf  3107  f1oprswap  5794  dmdcand  10310  modmul12d  11995  modnegd  11996  modadd12d  11997  exprec  12161  splval2  12696  eulerthlem2  14413  fermltl  14415  odzdvds  14423  efgredleme  16977  efgredlemc  16979  blssps  21111  blss  21112  metequiv2  21197  met1stc  21208  met2ndci  21209  metdstri  21539  xlebnum  21649  caubl  21930  divcxp  23254  cxple2a  23266  cxplead  23288  cxplt2d  23293  cxple2d  23294  mulcxpd  23295  ang180  23365  wilthlem2  23616  lgslem4  23847  lgsvalmod  23863  lgsmod  23869  lgsdir2lem4  23874  lgsdirprm  23877  lgsne0  23881  lgseisen  23901  ax5seglem9  24538  xrsmulgzz  27998  heiborlem8  31577  cdlemd4  33200  cdleme15a  33273  cdleme17b  33286  cdleme25a  33353  cdleme25c  33355  cdleme25dN  33356  cdleme26ee  33360  tendococl  33772  tendodi1  33784  tendodi2  33785  cdlemi  33820  tendocan  33824  cdlemk5a  33835  cdlemk5  33836  cdlemk10  33843  cdlemk5u  33861  cdlemkfid1N  33921  pellexlem6  35112  rpexpmord  35226  acongeq  35263  jm2.25  35284  stoweidlem42  37174  stoweidlem51  37183  ldepspr  38565
  Copyright terms: Public domain W3C validator