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

Theorem syl221anc 1229
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 1224 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  syl222anc  1234  vtocldf  3021  f1oprswap  5680  dmdcand  10136  modmul12d  11753  modnegd  11754  modadd12d  11755  exprec  11905  splval2  12399  eulerthlem2  13857  fermltl  13859  odzdvds  13867  efgredleme  16240  efgredlemc  16242  blssps  19999  blss  20000  metequiv2  20085  met1stc  20096  met2ndci  20097  metdstri  20427  xlebnum  20537  caubl  20818  divcxp  22132  cxple2a  22144  cxplead  22166  cxplt2d  22171  cxple2d  22172  mulcxpd  22173  ang180  22210  wilthlem2  22407  lgslem4  22638  lgsvalmod  22654  lgsmod  22660  lgsdir2lem4  22665  lgsdirprm  22668  lgsne0  22672  lgseisen  22692  ax5seglem9  23183  xrsmulgzz  26139  heiborlem8  28717  pellexlem6  29175  rpexpmord  29289  acongeq  29326  jm2.25  29348  stoweidlem42  29837  stoweidlem51  29846  ldepspr  31007  cdlemd4  33845  cdleme15a  33918  cdleme17b  33931  cdleme25a  33997  cdleme25c  33999  cdleme25dN  34000  cdleme26ee  34004  tendococl  34416  tendodi1  34428  tendodi2  34429  cdlemi  34464  tendocan  34468  cdlemk5a  34479  cdlemk5  34480  cdlemk10  34487  cdlemk5u  34505  cdlemkfid1N  34565
  Copyright terms: Public domain W3C validator