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

Theorem syl221anc 1193
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 518 . 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 1188 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  syl222anc  1198  vtocldf  2848  iota2df  5259  f1oprswap  5531  riotasv2dOLD  6366  dmdcand  9581  modmul12d  11019  modnegd  11020  modadd12d  11021  exprec  11159  splval2  11488  eulerthlem2  12866  fermltl  12868  odzdvds  12876  efgredleme  15068  efgredlemc  15070  blss  17988  metequiv2  18072  met1stc  18083  met2ndci  18084  metdstri  18371  xlebnum  18479  caubl  18749  divcxp  20050  cxple2a  20062  cxplead  20084  cxplt2d  20089  cxple2d  20090  mulcxpd  20091  ang180  20128  wilthlem2  20323  lgslem4  20554  lgsvalmod  20570  lgsmod  20576  lgsdir2lem4  20581  lgsdirprm  20584  lgsne0  20588  lgseisen  20608  xrsmulgzz  23322  ax5seglem9  24637  gapm2  25472  heiborlem8  26645  pellexlem6  27022  rpexpmord  27136  acongeq  27173  jm2.25  27195  cdlemd4  31012  cdleme15a  31085  cdleme17b  31098  cdleme25a  31164  cdleme25c  31166  cdleme25dN  31167  cdleme26ee  31171  tendococl  31583  tendodi1  31595  tendodi2  31596  cdlemi  31631  tendocan  31635  cdlemk5a  31646  cdlemk5  31647  cdlemk10  31654  cdlemk5u  31672  cdlemkfid1N  31732
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator