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

Theorem syl122anc 1227
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 532 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl122anc.6 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl121anc 1223 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:  divdiv32d  10124  divcan5d  10125  divcan7d  10127  divdiv1d  10130  divdiv2d  10131  seqcoll  12208  wrdeqswrdlsw  12335  cau3lem  12834  eqsqrd  12847  isercolllem2  13135  isercoll  13137  summolem2a  13184  divrcnv  13307  prmind2  13766  divnumden  13818  pceulem  13904  pcqmul  13912  pcqdiv  13916  pcexp  13918  pcaddlem  13942  pcbc  13954  latledi  15251  latjjdi  15265  latjjdir  15266  sylow1lem1  16088  sylow1lem5  16092  efgred2  16241  abladdsub4  16294  ablpnpcan  16300  ghmplusg  16319  frgpnabllem2  16343  isabvd  16883  lmodvs1  16954  lspsolvlem  17200  evlslem1  17576  frgpcyg  17981  ip2di  18045  mdetuni0  18402  elptr2  19122  qtophmeo  19365  blss2ps  19953  blss2  19954  blssps  19974  blss  19975  xmeter  19983  metdcnlem  20388  lebnumii  20513  minveclem2  20888  pjthlem1  20899  volfiniun  21003  dvfsumrlimge0  21477  lgsdi  22646  ax5seglem3  23128  ax5seglem6  23131  axcontlem8  23168  gxdi  23734  vacn  24040  minvecolem2  24227  minvecolem4  24232  disjabrex  25877  disjabrexf  25878  slmdvs1  26187  slmd0vs  26191  ornglmulle  26224  orngrmulle  26225  orngmullt  26228  prodmolem2a  27398  cgrcomand  27973  cgrcomr  27979  cgrcomland  27981  cgrcomrand  27982  cgrtriv  27984  cgrid2  27985  ofscom  27989  cgrextend  27990  segconeq  27992  btwntriv2  27994  btwnexch3and  28003  btwnouttr2  28004  btwnouttr  28006  btwnexch  28007  btwnexchand  28008  btwndiff  28009  ifscgr  28026  cgrsub  28027  cgrxfr  28037  lineext  28058  endofsegid  28067  btwnconn1lem2  28070  btwnconn1lem3  28071  btwnconn1lem4  28072  btwnconn1lem5  28073  btwnconn1lem7  28075  btwnconn1lem8  28076  btwnconn1lem10  28078  btwnconn1lem11  28079  btwnconn1lem13  28081  btwnconn1lem14  28082  btwnconn3  28085  midofsegid  28086  segcon2  28087  brsegle2  28091  seglecgr12im  28092  seglecgr12  28093  seglerflx  28094  seglemin  28095  segletr  28096  btwnsegle  28099  colinbtwnle  28100  btwnoutside  28107  broutsideof3  28108  outsideoftr  28111  outsideofeq  28112  outsidele  28114  lineunray  28129  lineelsb2  28130  pellfundex  29180  rmxypairf1o  29205  rmxycomplete  29211  rmxyneg  29214  rmxyadd  29215  rmxy1  29216  rmxy0  29217  jm2.22  29297  proot1mul  29517  deg1mhm  29528  stoweidlem7  29755  stoweidlem36  29784  lfladdcl  32556  lshpkrlem4  32598  latmmdiN  32719  latmmdir  32720  hlatj4  32858  4atlem4b  33084  4atlem11  33093  4atlem12  33096  dalem2  33145  dalem-cly  33155  dalem10  33157  dalem23  33180  dalem38  33194  dalem44  33200  dalem55  33211  cdlema1N  33275  paddclN  33326  pmapjoin  33336  dalawlem3  33357  dalawlem5  33359  dalawlem7  33361  dalawlem8  33362  dalawlem11  33365  dalawlem12  33366  lhpexle3lem  33495  4atexlemc  33553  trlnidat  33657  arglem1N  33674  cdlemd9  33690  cdleme0moN  33709  cdleme11c  33745  cdleme11h  33750  cdleme11  33754  cdleme16c  33764  cdleme16f  33767  cdlemeda  33782  cdleme20l2  33805  cdlemefs32sn1aw  33898  cdleme43fsv1snlem  33904  cdleme41sn3a  33917  cdleme32fva  33921  cdleme32b  33926  cdleme32c  33927  cdleme32e  33929  cdleme40m  33951  cdleme40n  33952  cdleme42e  33963  cdleme48d  34019  cdlemf2  34046  cdlemf  34047  cdlemg2fv2  34084  cdlemg7fvbwN  34091  cdlemg7fvN  34108  cdlemg9a  34116  cdlemg9b  34117  cdlemg10a  34124  cdlemg12b  34128  cdlemg17b  34146  cdlemg31d  34184  cdlemg33b0  34185  cdlemg33a  34190  ltrnco  34203  ltrncom  34222  cdlemh  34301  cdlemk3  34317  cdlemk12  34334  cdlemk12u  34356  cdlemkfid1N  34405  cdlemk51  34437  cdlemk54  34442  cdlemk43N  34447  cdlemk35u  34448  cdlemk55u1  34449  cdlemk39u1  34451  cdlemk19u1  34453  dia2dimlem10  34558  dvhgrp  34592  dvh0g  34596  cdlemm10N  34603  diblsmopel  34656  cdlemn4  34683  cdlemn6  34687  cdlemn7  34688  dihordlem7  34699  dihord1  34703  dihord2pre  34710  dihvalcqat  34724  dihopelvalcpre  34733  dihord5apre  34747  dihord  34749  dih1  34771  dihglbcpreN  34785  dihjatc1  34796  dihmeetlem13N  34804  dihmeetALTN  34812  dihjatcclem1  34903  baerlem3lem1  35192
  Copyright terms: Public domain W3C validator