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

Theorem syl122anc 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 )
syl122anc.6  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et ) )  ->  ze )
Assertion
Ref Expression
syl122anc  |-  ( ph  ->  ze )

Proof of Theorem syl122anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
64, 5jca 519 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl122anc.6 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl121anc 1189 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  divdiv32d  9815  divcan5d  9816  divcan7d  9818  divdiv1d  9821  divdiv2d  9822  seqcoll  11712  cau3lem  12158  eqsqrd  12171  isercolllem2  12459  isercoll  12461  summolem2a  12509  divrcnv  12632  prmind2  13090  divnumden  13140  pceulem  13219  pcqmul  13227  pcqdiv  13231  pcexp  13233  pcaddlem  13257  pcbc  13269  latledi  14518  latjjdi  14532  latjjdir  14533  sylow1lem1  15232  sylow1lem5  15236  efgred2  15385  abladdsub4  15438  ablpnpcan  15444  ghmplusg  15461  frgpnabllem2  15485  isabvd  15908  lmodvs1  15978  lspsolvlem  16214  frgpcyg  16854  ip2di  16872  elptr2  17606  qtophmeo  17849  blss2ps  18433  blss2  18434  blssps  18454  blss  18455  xmeter  18463  metdcnlem  18867  lebnumii  18991  minveclem2  19327  pjthlem1  19338  volfiniun  19441  dvfsumrlimge0  19914  evlslem1  19936  lgsdi  21116  gxdi  21884  vacn  22190  minvecolem2  22377  minvecolem4  22382  disjabrex  24024  disjabrexf  24025  ofldsqr  24240  prodmolem2a  25260  ax5seglem3  25870  ax5seglem6  25873  axcontlem8  25910  cgrcomand  25925  cgrcomr  25931  cgrcomland  25933  cgrcomrand  25934  cgrtriv  25936  cgrid2  25937  ofscom  25941  cgrextend  25942  segconeq  25944  btwntriv2  25946  btwnexch3and  25955  btwnouttr2  25956  btwnouttr  25958  btwnexch  25959  btwnexchand  25960  btwndiff  25961  ifscgr  25978  cgrsub  25979  cgrxfr  25989  lineext  26010  endofsegid  26019  btwnconn1lem2  26022  btwnconn1lem3  26023  btwnconn1lem4  26024  btwnconn1lem5  26025  btwnconn1lem7  26027  btwnconn1lem8  26028  btwnconn1lem10  26030  btwnconn1lem11  26031  btwnconn1lem13  26033  btwnconn1lem14  26034  btwnconn3  26037  midofsegid  26038  segcon2  26039  brsegle2  26043  seglecgr12im  26044  seglecgr12  26045  seglerflx  26046  seglemin  26047  segletr  26048  btwnsegle  26051  colinbtwnle  26052  btwnoutside  26059  broutsideof3  26060  outsideoftr  26063  outsideofeq  26064  outsidele  26066  lineunray  26081  lineelsb2  26082  pellfundex  26949  rmxypairf1o  26974  rmxycomplete  26980  rmxyneg  26983  rmxyadd  26984  rmxy1  26985  rmxy0  26986  jm2.22  27066  proot1mul  27492  deg1mhm  27503  stoweidlem7  27732  stoweidlem36  27761  lfladdcl  29869  lshpkrlem4  29911  latmmdiN  30032  latmmdir  30033  hlatj4  30171  4atlem4b  30397  4atlem11  30406  4atlem12  30409  dalem2  30458  dalem-cly  30468  dalem10  30470  dalem23  30493  dalem38  30507  dalem44  30513  dalem55  30524  cdlema1N  30588  paddclN  30639  pmapjoin  30649  dalawlem3  30670  dalawlem5  30672  dalawlem7  30674  dalawlem8  30675  dalawlem11  30678  dalawlem12  30679  lhpexle3lem  30808  4atexlemc  30866  trlnidat  30970  arglem1N  30987  cdlemd9  31003  cdleme0moN  31022  cdleme11c  31058  cdleme11h  31063  cdleme11  31067  cdleme16c  31077  cdleme16f  31080  cdlemeda  31095  cdleme20l2  31118  cdlemefs32sn1aw  31211  cdleme43fsv1snlem  31217  cdleme41sn3a  31230  cdleme32fva  31234  cdleme32b  31239  cdleme32c  31240  cdleme32e  31242  cdleme40m  31264  cdleme40n  31265  cdleme42e  31276  cdleme48d  31332  cdlemf2  31359  cdlemf  31360  cdlemg2fv2  31397  cdlemg7fvbwN  31404  cdlemg7fvN  31421  cdlemg9a  31429  cdlemg9b  31430  cdlemg10a  31437  cdlemg12b  31441  cdlemg17b  31459  cdlemg31d  31497  cdlemg33b0  31498  cdlemg33a  31503  ltrnco  31516  ltrncom  31535  cdlemh  31614  cdlemk3  31630  cdlemk12  31647  cdlemk12u  31669  cdlemkfid1N  31718  cdlemk51  31750  cdlemk54  31755  cdlemk43N  31760  cdlemk35u  31761  cdlemk55u1  31762  cdlemk39u1  31764  cdlemk19u1  31766  dia2dimlem10  31871  dvhgrp  31905  dvh0g  31909  cdlemm10N  31916  diblsmopel  31969  cdlemn4  31996  cdlemn6  32000  cdlemn7  32001  dihordlem7  32012  dihord1  32016  dihord2pre  32023  dihvalcqat  32037  dihopelvalcpre  32046  dihord5apre  32060  dihord  32062  dih1  32084  dihglbcpreN  32098  dihjatc1  32109  dihmeetlem13N  32117  dihmeetALTN  32125  dihjatcclem1  32216  baerlem3lem1  32505
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator