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  2835  iota2df  5243  f1oprswap  5515  riotasv2dOLD  6350  dmdcand  9565  modmul12d  11003  modnegd  11004  modadd12d  11005  exprec  11143  splval2  11472  eulerthlem2  12850  fermltl  12852  odzdvds  12860  efgredleme  15052  efgredlemc  15054  blss  17972  metequiv2  18056  met1stc  18067  met2ndci  18068  metdstri  18355  xlebnum  18463  caubl  18733  divcxp  20034  cxple2a  20046  cxplead  20068  cxplt2d  20073  cxple2d  20074  mulcxpd  20075  ang180  20112  wilthlem2  20307  lgslem4  20538  lgsvalmod  20554  lgsmod  20560  lgsdir2lem4  20565  lgsdirprm  20568  lgsne0  20572  lgseisen  20592  xrsmulgzz  23307  ax5seglem9  24565  gapm2  25369  heiborlem8  26542  pellexlem6  26919  rpexpmord  27033  acongeq  27070  jm2.25  27092  cdlemd4  30390  cdleme15a  30463  cdleme17b  30476  cdleme25a  30542  cdleme25c  30544  cdleme25dN  30545  cdleme26ee  30549  tendococl  30961  tendodi1  30973  tendodi2  30974  cdlemi  31009  tendocan  31013  cdlemk5a  31024  cdlemk5  31025  cdlemk10  31032  cdlemk5u  31050  cdlemkfid1N  31110
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