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

Theorem syl122anc 1237
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 1233 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  divdiv32d  10344  divcan5d  10345  divcan7d  10347  divdiv1d  10350  divdiv2d  10351  seqcoll  12477  wrdeqswrdlsw  12636  cau3lem  13149  eqsqrtd  13162  isercolllem2  13450  isercoll  13452  summolem2a  13499  divrcnv  13626  prmind2  14086  divnumden  14139  pceulem  14227  pcqmul  14235  pcqdiv  14239  pcexp  14241  pcaddlem  14265  pcbc  14277  latledi  15575  latjjdi  15589  latjjdir  15590  sylow1lem1  16421  sylow1lem5  16425  efgred2  16574  abladdsub4  16627  ablpnpcan  16633  ghmplusg  16652  frgpnabllem2  16678  isabvd  17264  lmodvs1  17335  lspsolvlem  17583  evlslem1  17971  frgpcyg  18395  ip2di  18459  mdetuni0  18906  cpmadugsumlemB  19158  elptr2  19826  qtophmeo  20069  blss2ps  20657  blss2  20658  blssps  20678  blss  20679  xmeter  20687  metdcnlem  21092  lebnumii  21217  minveclem2  21592  pjthlem1  21603  volfiniun  21708  dvfsumrlimge0  22182  lgsdi  23351  ax5seglem3  23926  ax5seglem6  23929  axcontlem8  23966  gxdi  24990  vacn  25296  minvecolem2  25483  minvecolem4  25488  disjabrex  27132  disjabrexf  27133  slmdvs1  27441  slmd0vs  27445  ornglmulle  27474  orngrmulle  27475  orngmullt  27478  prodmolem2a  28659  cgrcomand  29234  cgrcomr  29240  cgrcomland  29242  cgrcomrand  29243  cgrtriv  29245  cgrid2  29246  ofscom  29250  cgrextend  29251  segconeq  29253  btwntriv2  29255  btwnexch3and  29264  btwnouttr2  29265  btwnouttr  29267  btwnexch  29268  btwnexchand  29269  btwndiff  29270  ifscgr  29287  cgrsub  29288  cgrxfr  29298  lineext  29319  endofsegid  29328  btwnconn1lem2  29331  btwnconn1lem3  29332  btwnconn1lem4  29333  btwnconn1lem5  29334  btwnconn1lem7  29336  btwnconn1lem8  29337  btwnconn1lem10  29339  btwnconn1lem11  29340  btwnconn1lem13  29342  btwnconn1lem14  29343  btwnconn3  29346  midofsegid  29347  segcon2  29348  brsegle2  29352  seglecgr12im  29353  seglecgr12  29354  seglerflx  29355  seglemin  29356  segletr  29357  btwnsegle  29360  colinbtwnle  29361  btwnoutside  29368  broutsideof3  29369  outsideoftr  29372  outsideofeq  29373  outsidele  29375  lineunray  29390  lineelsb2  29391  pellfundex  30442  rmxypairf1o  30467  rmxycomplete  30473  rmxyneg  30476  rmxyadd  30477  rmxy1  30478  rmxy0  30479  jm2.22  30557  proot1mul  30777  deg1mhm  30788  stoweidlem7  31323  stoweidlem36  31352  lfladdcl  33877  lshpkrlem4  33919  latmmdiN  34040  latmmdir  34041  hlatj4  34179  4atlem4b  34405  4atlem11  34414  4atlem12  34417  dalem2  34466  dalem-cly  34476  dalem10  34478  dalem23  34501  dalem38  34515  dalem44  34521  dalem55  34532  cdlema1N  34596  paddclN  34647  pmapjoin  34657  dalawlem3  34678  dalawlem5  34680  dalawlem7  34682  dalawlem8  34683  dalawlem11  34686  dalawlem12  34687  lhpexle3lem  34816  4atexlemc  34874  trlnidat  34978  arglem1N  34995  cdlemd9  35011  cdleme0moN  35030  cdleme11c  35066  cdleme11h  35071  cdleme11  35075  cdleme16c  35085  cdleme16f  35088  cdlemeda  35103  cdleme20l2  35126  cdlemefs32sn1aw  35219  cdleme43fsv1snlem  35225  cdleme41sn3a  35238  cdleme32fva  35242  cdleme32b  35247  cdleme32c  35248  cdleme32e  35250  cdleme40m  35272  cdleme40n  35273  cdleme42e  35284  cdleme48d  35340  cdlemf2  35367  cdlemf  35368  cdlemg2fv2  35405  cdlemg7fvbwN  35412  cdlemg7fvN  35429  cdlemg9a  35437  cdlemg9b  35438  cdlemg10a  35445  cdlemg12b  35449  cdlemg17b  35467  cdlemg31d  35505  cdlemg33b0  35506  cdlemg33a  35511  ltrnco  35524  ltrncom  35543  cdlemh  35622  cdlemk3  35638  cdlemk12  35655  cdlemk12u  35677  cdlemkfid1N  35726  cdlemk51  35758  cdlemk54  35763  cdlemk43N  35768  cdlemk35u  35769  cdlemk55u1  35770  cdlemk39u1  35772  cdlemk19u1  35774  dia2dimlem10  35879  dvhgrp  35913  dvh0g  35917  cdlemm10N  35924  diblsmopel  35977  cdlemn4  36004  cdlemn6  36008  cdlemn7  36009  dihordlem7  36020  dihord1  36024  dihord2pre  36031  dihvalcqat  36045  dihopelvalcpre  36054  dihord5apre  36068  dihord  36070  dih1  36092  dihglbcpreN  36106  dihjatc1  36117  dihmeetlem13N  36125  dihmeetALTN  36133  dihjatcclem1  36224  baerlem3lem1  36513
  Copyright terms: Public domain W3C validator