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

Theorem syl122anc 1193
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 519 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl122anc.6 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl121anc 1189 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  divdiv32d  9771  divcan5d  9772  divcan7d  9774  divdiv1d  9777  divdiv2d  9778  seqcoll  11667  cau3lem  12113  eqsqrd  12126  isercolllem2  12414  isercoll  12416  summolem2a  12464  divrcnv  12587  prmind2  13045  divnumden  13095  pceulem  13174  pcqmul  13182  pcqdiv  13186  pcexp  13188  pcaddlem  13212  pcbc  13224  latledi  14473  latjjdi  14487  latjjdir  14488  sylow1lem1  15187  sylow1lem5  15191  efgred2  15340  abladdsub4  15393  ablpnpcan  15399  ghmplusg  15416  frgpnabllem2  15440  isabvd  15863  lmodvs1  15933  lspsolvlem  16169  frgpcyg  16809  ip2di  16827  elptr2  17559  qtophmeo  17802  blss2ps  18386  blss2  18387  blssps  18407  blss  18408  xmeter  18416  metdcnlem  18820  lebnumii  18944  minveclem2  19280  pjthlem1  19291  volfiniun  19394  dvfsumrlimge0  19867  evlslem1  19889  lgsdi  21069  gxdi  21837  vacn  22143  minvecolem2  22330  minvecolem4  22335  disjabrex  23977  disjabrexf  23978  ofldsqr  24193  prodmolem2a  25213  ax5seglem3  25774  ax5seglem6  25777  axcontlem8  25814  cgrcomand  25829  cgrcomr  25835  cgrcomland  25837  cgrcomrand  25838  cgrtriv  25840  cgrid2  25841  ofscom  25845  cgrextend  25846  segconeq  25848  btwntriv2  25850  btwnexch3and  25859  btwnouttr2  25860  btwnouttr  25862  btwnexch  25863  btwnexchand  25864  btwndiff  25865  ifscgr  25882  cgrsub  25883  cgrxfr  25893  lineext  25914  endofsegid  25923  btwnconn1lem2  25926  btwnconn1lem3  25927  btwnconn1lem4  25928  btwnconn1lem5  25929  btwnconn1lem7  25931  btwnconn1lem8  25932  btwnconn1lem10  25934  btwnconn1lem11  25935  btwnconn1lem13  25937  btwnconn1lem14  25938  btwnconn3  25941  midofsegid  25942  segcon2  25943  brsegle2  25947  seglecgr12im  25948  seglecgr12  25949  seglerflx  25950  seglemin  25951  segletr  25952  btwnsegle  25955  colinbtwnle  25956  btwnoutside  25963  broutsideof3  25964  outsideoftr  25967  outsideofeq  25968  outsidele  25970  lineunray  25985  lineelsb2  25986  pellfundex  26839  rmxypairf1o  26864  rmxycomplete  26870  rmxyneg  26873  rmxyadd  26874  rmxy1  26875  rmxy0  26876  jm2.22  26956  proot1mul  27383  deg1mhm  27394  stoweidlem7  27623  stoweidlem36  27652  lfladdcl  29554  lshpkrlem4  29596  latmmdiN  29717  latmmdir  29718  hlatj4  29856  4atlem4b  30082  4atlem11  30091  4atlem12  30094  dalem2  30143  dalem-cly  30153  dalem10  30155  dalem23  30178  dalem38  30192  dalem44  30198  dalem55  30209  cdlema1N  30273  paddclN  30324  pmapjoin  30334  dalawlem3  30355  dalawlem5  30357  dalawlem7  30359  dalawlem8  30360  dalawlem11  30363  dalawlem12  30364  lhpexle3lem  30493  4atexlemc  30551  trlnidat  30655  arglem1N  30672  cdlemd9  30688  cdleme0moN  30707  cdleme11c  30743  cdleme11h  30748  cdleme11  30752  cdleme16c  30762  cdleme16f  30765  cdlemeda  30780  cdleme20l2  30803  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme41sn3a  30915  cdleme32fva  30919  cdleme32b  30924  cdleme32c  30925  cdleme32e  30927  cdleme40m  30949  cdleme40n  30950  cdleme42e  30961  cdleme48d  31017  cdlemf2  31044  cdlemf  31045  cdlemg2fv2  31082  cdlemg7fvbwN  31089  cdlemg7fvN  31106  cdlemg9a  31114  cdlemg9b  31115  cdlemg10a  31122  cdlemg12b  31126  cdlemg17b  31144  cdlemg31d  31182  cdlemg33b0  31183  cdlemg33a  31188  ltrnco  31201  ltrncom  31220  cdlemh  31299  cdlemk3  31315  cdlemk12  31332  cdlemk12u  31354  cdlemkfid1N  31403  cdlemk51  31435  cdlemk54  31440  cdlemk43N  31445  cdlemk35u  31446  cdlemk55u1  31447  cdlemk39u1  31449  cdlemk19u1  31451  dia2dimlem10  31556  dvhgrp  31590  dvh0g  31594  cdlemm10N  31601  diblsmopel  31654  cdlemn4  31681  cdlemn6  31685  cdlemn7  31686  dihordlem7  31697  dihord1  31701  dihord2pre  31708  dihvalcqat  31722  dihopelvalcpre  31731  dihord5apre  31745  dihord  31747  dih1  31769  dihglbcpreN  31783  dihjatc1  31794  dihmeetlem13N  31802  dihmeetALTN  31810  dihjatcclem1  31901  baerlem3lem1  32190
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator