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

Theorem syl122anc 1220
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 529 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl122anc.6 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl121anc 1216 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  divdiv32d  10119  divcan5d  10120  divcan7d  10122  divdiv1d  10125  divdiv2d  10126  seqcoll  12199  wrdeqswrdlsw  12326  cau3lem  12825  eqsqrd  12838  isercolllem2  13126  isercoll  13128  summolem2a  13175  divrcnv  13297  prmind2  13756  divnumden  13808  pceulem  13894  pcqmul  13902  pcqdiv  13906  pcexp  13908  pcaddlem  13932  pcbc  13944  latledi  15241  latjjdi  15255  latjjdir  15256  sylow1lem1  16076  sylow1lem5  16080  efgred2  16229  abladdsub4  16282  ablpnpcan  16288  ghmplusg  16307  frgpnabllem2  16331  isabvd  16828  lmodvs1  16899  lspsolvlem  17144  frgpcyg  17847  ip2di  17911  mdetuni0  18268  elptr2  18988  qtophmeo  19231  blss2ps  19819  blss2  19820  blssps  19840  blss  19841  xmeter  19849  metdcnlem  20254  lebnumii  20379  minveclem2  20754  pjthlem1  20765  volfiniun  20869  dvfsumrlimge0  21343  evlslem1  21366  lgsdi  22555  ax5seglem3  22999  ax5seglem6  23002  axcontlem8  23039  gxdi  23605  vacn  23911  minvecolem2  24098  minvecolem4  24103  disjabrex  25749  disjabrexf  25750  slmdvs1  26084  slmd0vs  26088  ornglmulle  26125  orngrmulle  26126  orngmullt  26129  prodmolem2a  27293  cgrcomand  27868  cgrcomr  27874  cgrcomland  27876  cgrcomrand  27877  cgrtriv  27879  cgrid2  27880  ofscom  27884  cgrextend  27885  segconeq  27887  btwntriv2  27889  btwnexch3and  27898  btwnouttr2  27899  btwnouttr  27901  btwnexch  27902  btwnexchand  27903  btwndiff  27904  ifscgr  27921  cgrsub  27922  cgrxfr  27932  lineext  27953  endofsegid  27962  btwnconn1lem2  27965  btwnconn1lem3  27966  btwnconn1lem4  27967  btwnconn1lem5  27968  btwnconn1lem7  27970  btwnconn1lem8  27971  btwnconn1lem10  27973  btwnconn1lem11  27974  btwnconn1lem13  27976  btwnconn1lem14  27977  btwnconn3  27980  midofsegid  27981  segcon2  27982  brsegle2  27986  seglecgr12im  27987  seglecgr12  27988  seglerflx  27989  seglemin  27990  segletr  27991  btwnsegle  27994  colinbtwnle  27995  btwnoutside  28002  broutsideof3  28003  outsideoftr  28006  outsideofeq  28007  outsidele  28009  lineunray  28024  lineelsb2  28025  pellfundex  29069  rmxypairf1o  29094  rmxycomplete  29100  rmxyneg  29103  rmxyadd  29104  rmxy1  29105  rmxy0  29106  jm2.22  29186  proot1mul  29406  deg1mhm  29417  stoweidlem7  29645  stoweidlem36  29674  lfladdcl  32286  lshpkrlem4  32328  latmmdiN  32449  latmmdir  32450  hlatj4  32588  4atlem4b  32814  4atlem11  32823  4atlem12  32826  dalem2  32875  dalem-cly  32885  dalem10  32887  dalem23  32910  dalem38  32924  dalem44  32930  dalem55  32941  cdlema1N  33005  paddclN  33056  pmapjoin  33066  dalawlem3  33087  dalawlem5  33089  dalawlem7  33091  dalawlem8  33092  dalawlem11  33095  dalawlem12  33096  lhpexle3lem  33225  4atexlemc  33283  trlnidat  33387  arglem1N  33404  cdlemd9  33420  cdleme0moN  33439  cdleme11c  33475  cdleme11h  33480  cdleme11  33484  cdleme16c  33494  cdleme16f  33497  cdlemeda  33512  cdleme20l2  33535  cdlemefs32sn1aw  33628  cdleme43fsv1snlem  33634  cdleme41sn3a  33647  cdleme32fva  33651  cdleme32b  33656  cdleme32c  33657  cdleme32e  33659  cdleme40m  33681  cdleme40n  33682  cdleme42e  33693  cdleme48d  33749  cdlemf2  33776  cdlemf  33777  cdlemg2fv2  33814  cdlemg7fvbwN  33821  cdlemg7fvN  33838  cdlemg9a  33846  cdlemg9b  33847  cdlemg10a  33854  cdlemg12b  33858  cdlemg17b  33876  cdlemg31d  33914  cdlemg33b0  33915  cdlemg33a  33920  ltrnco  33933  ltrncom  33952  cdlemh  34031  cdlemk3  34047  cdlemk12  34064  cdlemk12u  34086  cdlemkfid1N  34135  cdlemk51  34167  cdlemk54  34172  cdlemk43N  34177  cdlemk35u  34178  cdlemk55u1  34179  cdlemk39u1  34181  cdlemk19u1  34183  dia2dimlem10  34288  dvhgrp  34322  dvh0g  34326  cdlemm10N  34333  diblsmopel  34386  cdlemn4  34413  cdlemn6  34417  cdlemn7  34418  dihordlem7  34429  dihord1  34433  dihord2pre  34440  dihvalcqat  34454  dihopelvalcpre  34463  dihord5apre  34477  dihord  34479  dih1  34501  dihglbcpreN  34515  dihjatc1  34526  dihmeetlem13N  34534  dihmeetALTN  34542  dihjatcclem1  34633  baerlem3lem1  34922
  Copyright terms: Public domain W3C validator