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  10359  divcan5d  10360  divcan7d  10362  divdiv1d  10365  divdiv2d  10366  seqcoll  12575  cau3lem  13361  eqsqrtd  13374  isercolllem2  13672  isercoll  13674  summolem2a  13724  divrcnv  13853  prodmolem2a  13931  prmind2  14578  divnumden  14640  pceulem  14738  pcqmul  14746  pcqdiv  14750  pcexp  14752  pcaddlem  14776  pcbc  14788  prmodvdslcmf  14948  prmordvdslcmfOLD  14962  prmordvdslcmsOLDOLD  14964  latledi  16278  latjjdi  16292  latjjdir  16293  sylow1lem1  17193  sylow1lem5  17197  efgred2  17346  abladdsub4  17399  ablpnpcan  17405  ghmplusg  17427  frgpnabllem2  17453  isabvd  17991  lmodvs1  18062  lspsolvlem  18308  evlslem1  18681  frgpcyg  19086  ip2di  19150  mdetuni0  19588  cpmadugsumlemB  19840  elptr2  20531  blss2ps  21360  blss2  21361  blssps  21381  blss  21382  xmeter  21390  metdcnlem  21796  lebnumii  21939  minveclem2  22310  minveclem2OLD  22322  pjthlem1  22333  volfiniun  22442  dvfsumrlimge0  22924  lgsdi  24202  ax5seglem3  24903  ax5seglem6  24906  axcontlem8  24943  eengtrkg  24957  gxdi  25966  vacn  26272  minvecolem2  26459  minvecolem4  26464  minvecolem2OLD  26469  minvecolem4OLD  26474  disjabrex  28138  disjabrexf  28139  slmdvs1  28487  slmd0vs  28491  orngsqr  28519  ornglmulle  28520  orngrmulle  28521  orngmullt  28524  suborng  28530  madjusmdetlem1  28605  cgrcomand  30707  cgrcomr  30713  cgrcomland  30715  cgrcomrand  30716  cgrtriv  30718  cgrid2  30719  ofscom  30723  cgrextend  30724  segconeq  30726  btwntriv2  30728  btwnexch3and  30737  btwnouttr2  30738  btwnouttr  30740  btwnexch  30741  btwnexchand  30742  btwndiff  30743  ifscgr  30760  cgrsub  30761  cgrxfr  30771  lineext  30792  endofsegid  30801  btwnconn1lem2  30804  btwnconn1lem3  30805  btwnconn1lem4  30806  btwnconn1lem5  30807  btwnconn1lem7  30809  btwnconn1lem8  30810  btwnconn1lem10  30812  btwnconn1lem11  30813  btwnconn1lem13  30815  btwnconn1lem14  30816  btwnconn3  30819  midofsegid  30820  segcon2  30821  brsegle2  30825  seglecgr12im  30826  seglecgr12  30827  seglerflx  30828  seglemin  30829  segletr  30830  btwnsegle  30833  colinbtwnle  30834  btwnoutside  30841  broutsideof3  30842  outsideoftr  30845  outsideofeq  30846  outsidele  30848  lineunray  30863  lineelsb2  30864  lfladdcl  32549  lshpkrlem4  32591  latmmdiN  32712  latmmdir  32713  hlatj4  32851  4atlem4b  33077  4atlem11  33086  4atlem12  33089  dalem2  33138  dalem-cly  33148  dalem10  33150  dalem23  33173  dalem38  33187  dalem44  33193  dalem55  33204  cdlema1N  33268  paddclN  33319  pmapjoin  33329  dalawlem3  33350  dalawlem5  33352  dalawlem7  33354  dalawlem8  33355  dalawlem11  33358  dalawlem12  33359  lhpexle3lem  33488  4atexlemc  33546  trlnidat  33651  arglem1N  33668  cdlemd9  33684  cdleme0moN  33703  cdleme11c  33739  cdleme11h  33744  cdleme11  33748  cdleme16c  33758  cdleme16f  33761  cdlemeda  33776  cdleme20l2  33800  cdlemefs32sn1aw  33893  cdleme43fsv1snlem  33899  cdleme41sn3a  33912  cdleme32fva  33916  cdleme32b  33921  cdleme32c  33922  cdleme32e  33924  cdleme40m  33946  cdleme40n  33947  cdleme42e  33958  cdleme48d  34014  cdlemf2  34041  cdlemf  34042  cdlemg2fv2  34079  cdlemg7fvbwN  34086  cdlemg7fvN  34103  cdlemg9a  34111  cdlemg9b  34112  cdlemg10a  34119  cdlemg12b  34123  cdlemg17b  34141  cdlemg31d  34179  cdlemg33b0  34180  cdlemg33a  34185  ltrnco  34198  ltrncom  34217  cdlemh  34296  cdlemk3  34312  cdlemk12  34329  cdlemk12u  34351  cdlemkfid1N  34400  cdlemk51  34432  cdlemk54  34437  cdlemk43N  34442  cdlemk35u  34443  cdlemk55u1  34444  cdlemk39u1  34446  cdlemk19u1  34448  dia2dimlem10  34553  dvhgrp  34587  dvh0g  34591  cdlemm10N  34598  diblsmopel  34651  cdlemn4  34678  cdlemn6  34682  cdlemn7  34683  dihordlem7  34694  dihord1  34698  dihord2pre  34705  dihvalcqat  34719  dihopelvalcpre  34728  dihord5apre  34742  dihord  34744  dih1  34766  dihglbcpreN  34780  dihjatc1  34791  dihmeetlem13N  34799  dihmeetALTN  34807  dihjatcclem1  34898  baerlem3lem1  35187  pellfundex  35647  rmxypairf1o  35672  rmxycomplete  35678  rmxyneg  35681  rmxyadd  35682  rmxy1  35683  rmxy0  35684  jm2.22  35763  proot1mul  35986  deg1mhm  35997  stoweidlem7  37750  stoweidlem36  37780
  Copyright terms: Public domain W3C validator