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

Theorem syl122anc 1238
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 1234 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 976
This theorem is referenced by:  divdiv32d  10352  divcan5d  10353  divcan7d  10355  divdiv1d  10358  divdiv2d  10359  seqcoll  12494  wrdeqswrdlsw  12656  cau3lem  13169  eqsqrtd  13182  isercolllem2  13470  isercoll  13472  summolem2a  13519  divrcnv  13646  prodmolem2a  13723  prmind2  14210  divnumden  14263  pceulem  14351  pcqmul  14359  pcqdiv  14363  pcexp  14365  pcaddlem  14389  pcbc  14401  latledi  15698  latjjdi  15712  latjjdir  15713  sylow1lem1  16597  sylow1lem5  16601  efgred2  16750  abladdsub4  16803  ablpnpcan  16809  ghmplusg  16831  frgpnabllem2  16857  isabvd  17448  lmodvs1  17519  lspsolvlem  17767  evlslem1  18163  frgpcyg  18590  ip2di  18654  mdetuni0  19101  cpmadugsumlemB  19353  elptr2  20053  blss2ps  20884  blss2  20885  blssps  20905  blss  20906  xmeter  20914  metdcnlem  21319  lebnumii  21444  minveclem2  21819  pjthlem1  21830  volfiniun  21935  dvfsumrlimge0  22409  lgsdi  23585  ax5seglem3  24212  ax5seglem6  24215  axcontlem8  24252  eengtrkg  24266  gxdi  25276  vacn  25582  minvecolem2  25769  minvecolem4  25774  disjabrex  27421  disjabrexf  27422  slmdvs1  27741  slmd0vs  27745  orngsqr  27772  ornglmulle  27773  orngrmulle  27774  orngmullt  27777  suborng  27783  cgrcomand  29617  cgrcomr  29623  cgrcomland  29625  cgrcomrand  29626  cgrtriv  29628  cgrid2  29629  ofscom  29633  cgrextend  29634  segconeq  29636  btwntriv2  29638  btwnexch3and  29647  btwnouttr2  29648  btwnouttr  29650  btwnexch  29651  btwnexchand  29652  btwndiff  29653  ifscgr  29670  cgrsub  29671  cgrxfr  29681  lineext  29702  endofsegid  29711  btwnconn1lem2  29714  btwnconn1lem3  29715  btwnconn1lem4  29716  btwnconn1lem5  29717  btwnconn1lem7  29719  btwnconn1lem8  29720  btwnconn1lem10  29722  btwnconn1lem11  29723  btwnconn1lem13  29725  btwnconn1lem14  29726  btwnconn3  29729  midofsegid  29730  segcon2  29731  brsegle2  29735  seglecgr12im  29736  seglecgr12  29737  seglerflx  29738  seglemin  29739  segletr  29740  btwnsegle  29743  colinbtwnle  29744  btwnoutside  29751  broutsideof3  29752  outsideoftr  29755  outsideofeq  29756  outsidele  29758  lineunray  29773  lineelsb2  29774  pellfundex  30798  rmxypairf1o  30823  rmxycomplete  30829  rmxyneg  30832  rmxyadd  30833  rmxy1  30834  rmxy0  30835  jm2.22  30913  proot1mul  31132  deg1mhm  31143  stoweidlem7  31743  stoweidlem36  31772  lfladdcl  34671  lshpkrlem4  34713  latmmdiN  34834  latmmdir  34835  hlatj4  34973  4atlem4b  35199  4atlem11  35208  4atlem12  35211  dalem2  35260  dalem-cly  35270  dalem10  35272  dalem23  35295  dalem38  35309  dalem44  35315  dalem55  35326  cdlema1N  35390  paddclN  35441  pmapjoin  35451  dalawlem3  35472  dalawlem5  35474  dalawlem7  35476  dalawlem8  35477  dalawlem11  35480  dalawlem12  35481  lhpexle3lem  35610  4atexlemc  35668  trlnidat  35773  arglem1N  35790  cdlemd9  35806  cdleme0moN  35825  cdleme11c  35861  cdleme11h  35866  cdleme11  35870  cdleme16c  35880  cdleme16f  35883  cdlemeda  35898  cdleme20l2  35922  cdlemefs32sn1aw  36015  cdleme43fsv1snlem  36021  cdleme41sn3a  36034  cdleme32fva  36038  cdleme32b  36043  cdleme32c  36044  cdleme32e  36046  cdleme40m  36068  cdleme40n  36069  cdleme42e  36080  cdleme48d  36136  cdlemf2  36163  cdlemf  36164  cdlemg2fv2  36201  cdlemg7fvbwN  36208  cdlemg7fvN  36225  cdlemg9a  36233  cdlemg9b  36234  cdlemg10a  36241  cdlemg12b  36245  cdlemg17b  36263  cdlemg31d  36301  cdlemg33b0  36302  cdlemg33a  36307  ltrnco  36320  ltrncom  36339  cdlemh  36418  cdlemk3  36434  cdlemk12  36451  cdlemk12u  36473  cdlemkfid1N  36522  cdlemk51  36554  cdlemk54  36559  cdlemk43N  36564  cdlemk35u  36565  cdlemk55u1  36566  cdlemk39u1  36568  cdlemk19u1  36570  dia2dimlem10  36675  dvhgrp  36709  dvh0g  36713  cdlemm10N  36720  diblsmopel  36773  cdlemn4  36800  cdlemn6  36804  cdlemn7  36805  dihordlem7  36816  dihord1  36820  dihord2pre  36827  dihvalcqat  36841  dihopelvalcpre  36850  dihord5apre  36864  dihord  36866  dih1  36888  dihglbcpreN  36902  dihjatc1  36913  dihmeetlem13N  36921  dihmeetALTN  36929  dihjatcclem1  37020  baerlem3lem1  37309
  Copyright terms: Public domain W3C validator