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

Theorem syl122anc 1273
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 534 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl122anc.6 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl121anc 1269 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  divdiv32d  10407  divcan5d  10408  divcan7d  10410  divdiv1d  10413  divdiv2d  10414  seqcoll  12621  cau3lem  13396  eqsqrtd  13409  isercolllem2  13707  isercoll  13709  summolem2a  13759  divrcnv  13888  prodmolem2a  13966  prmind2  14606  divnumden  14668  pceulem  14758  pcqmul  14766  pcqdiv  14770  pcexp  14772  pcaddlem  14796  pcbc  14808  prmodvdslcmf  14968  prmordvdslcmfOLD  14982  prmordvdslcmsOLDOLD  14984  latledi  16286  latjjdi  16300  latjjdir  16301  sylow1lem1  17185  sylow1lem5  17189  efgred2  17338  abladdsub4  17391  ablpnpcan  17397  ghmplusg  17419  frgpnabllem2  17445  isabvd  17983  lmodvs1  18054  lspsolvlem  18300  evlslem1  18673  frgpcyg  19075  ip2di  19139  mdetuni0  19577  cpmadugsumlemB  19829  elptr2  20520  blss2ps  21349  blss2  21350  blssps  21370  blss  21371  xmeter  21379  metdcnlem  21765  lebnumii  21890  minveclem2  22261  pjthlem1  22272  volfiniun  22377  dvfsumrlimge0  22859  lgsdi  24123  ax5seglem3  24807  ax5seglem6  24810  axcontlem8  24847  eengtrkg  24861  gxdi  25869  vacn  26175  minvecolem2  26362  minvecolem4  26367  disjabrex  28031  disjabrexf  28032  slmdvs1  28374  slmd0vs  28378  orngsqr  28406  ornglmulle  28407  orngrmulle  28408  orngmullt  28411  suborng  28417  madjusmdetlem1  28492  cgrcomand  30543  cgrcomr  30549  cgrcomland  30551  cgrcomrand  30552  cgrtriv  30554  cgrid2  30555  ofscom  30559  cgrextend  30560  segconeq  30562  btwntriv2  30564  btwnexch3and  30573  btwnouttr2  30574  btwnouttr  30576  btwnexch  30577  btwnexchand  30578  btwndiff  30579  ifscgr  30596  cgrsub  30597  cgrxfr  30607  lineext  30628  endofsegid  30637  btwnconn1lem2  30640  btwnconn1lem3  30641  btwnconn1lem4  30642  btwnconn1lem5  30643  btwnconn1lem7  30645  btwnconn1lem8  30646  btwnconn1lem10  30648  btwnconn1lem11  30649  btwnconn1lem13  30651  btwnconn1lem14  30652  btwnconn3  30655  midofsegid  30656  segcon2  30657  brsegle2  30661  seglecgr12im  30662  seglecgr12  30663  seglerflx  30664  seglemin  30665  segletr  30666  btwnsegle  30669  colinbtwnle  30670  btwnoutside  30677  broutsideof3  30678  outsideoftr  30681  outsideofeq  30682  outsidele  30684  lineunray  30699  lineelsb2  30700  lfladdcl  32345  lshpkrlem4  32387  latmmdiN  32508  latmmdir  32509  hlatj4  32647  4atlem4b  32873  4atlem11  32882  4atlem12  32885  dalem2  32934  dalem-cly  32944  dalem10  32946  dalem23  32969  dalem38  32983  dalem44  32989  dalem55  33000  cdlema1N  33064  paddclN  33115  pmapjoin  33125  dalawlem3  33146  dalawlem5  33148  dalawlem7  33150  dalawlem8  33151  dalawlem11  33154  dalawlem12  33155  lhpexle3lem  33284  4atexlemc  33342  trlnidat  33447  arglem1N  33464  cdlemd9  33480  cdleme0moN  33499  cdleme11c  33535  cdleme11h  33540  cdleme11  33544  cdleme16c  33554  cdleme16f  33557  cdlemeda  33572  cdleme20l2  33596  cdlemefs32sn1aw  33689  cdleme43fsv1snlem  33695  cdleme41sn3a  33708  cdleme32fva  33712  cdleme32b  33717  cdleme32c  33718  cdleme32e  33720  cdleme40m  33742  cdleme40n  33743  cdleme42e  33754  cdleme48d  33810  cdlemf2  33837  cdlemf  33838  cdlemg2fv2  33875  cdlemg7fvbwN  33882  cdlemg7fvN  33899  cdlemg9a  33907  cdlemg9b  33908  cdlemg10a  33915  cdlemg12b  33919  cdlemg17b  33937  cdlemg31d  33975  cdlemg33b0  33976  cdlemg33a  33981  ltrnco  33994  ltrncom  34013  cdlemh  34092  cdlemk3  34108  cdlemk12  34125  cdlemk12u  34147  cdlemkfid1N  34196  cdlemk51  34228  cdlemk54  34233  cdlemk43N  34238  cdlemk35u  34239  cdlemk55u1  34240  cdlemk39u1  34242  cdlemk19u1  34244  dia2dimlem10  34349  dvhgrp  34383  dvh0g  34387  cdlemm10N  34394  diblsmopel  34447  cdlemn4  34474  cdlemn6  34478  cdlemn7  34479  dihordlem7  34490  dihord1  34494  dihord2pre  34501  dihvalcqat  34515  dihopelvalcpre  34524  dihord5apre  34538  dihord  34540  dih1  34562  dihglbcpreN  34576  dihjatc1  34587  dihmeetlem13N  34595  dihmeetALTN  34603  dihjatcclem1  34694  baerlem3lem1  34983  pellfundex  35439  rmxypairf1o  35464  rmxycomplete  35470  rmxyneg  35473  rmxyadd  35474  rmxy1  35475  rmxy0  35476  jm2.22  35555  proot1mul  35771  deg1mhm  35782  stoweidlem7  37435  stoweidlem36  37465
  Copyright terms: Public domain W3C validator