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

Theorem syl221anc 1239
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 532 . 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 1234 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  syl222anc  1244  vtocldf  3162  f1oprswap  5853  dmdcand  10345  modmul12d  12004  modnegd  12005  modadd12d  12006  exprec  12169  splval2  12690  eulerthlem2  14164  fermltl  14166  odzdvds  14174  efgredleme  16554  efgredlemc  16556  blssps  20659  blss  20660  metequiv2  20745  met1stc  20756  met2ndci  20757  metdstri  21087  xlebnum  21197  caubl  21478  divcxp  22793  cxple2a  22805  cxplead  22827  cxplt2d  22832  cxple2d  22833  mulcxpd  22834  ang180  22871  wilthlem2  23068  lgslem4  23299  lgsvalmod  23315  lgsmod  23321  lgsdir2lem4  23326  lgsdirprm  23329  lgsne0  23333  lgseisen  23353  ax5seglem9  23913  xrsmulgzz  27325  heiborlem8  29915  pellexlem6  30372  rpexpmord  30486  acongeq  30523  jm2.25  30545  stoweidlem42  31342  stoweidlem51  31351  ldepspr  32147  cdlemd4  34997  cdleme15a  35070  cdleme17b  35083  cdleme25a  35149  cdleme25c  35151  cdleme25dN  35152  cdleme26ee  35156  tendococl  35568  tendodi1  35580  tendodi2  35581  cdlemi  35616  tendocan  35620  cdlemk5a  35631  cdlemk5  35632  cdlemk10  35639  cdlemk5u  35657  cdlemkfid1N  35717
  Copyright terms: Public domain W3C validator