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

Theorem syl122anc 1228
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 1224 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  divdiv32d  10246  divcan5d  10247  divcan7d  10249  divdiv1d  10252  divdiv2d  10253  seqcoll  12337  wrdeqswrdlsw  12464  cau3lem  12963  eqsqrd  12976  isercolllem2  13264  isercoll  13266  summolem2a  13313  divrcnv  13436  prmind2  13895  divnumden  13947  pceulem  14033  pcqmul  14041  pcqdiv  14045  pcexp  14047  pcaddlem  14071  pcbc  14083  latledi  15381  latjjdi  15395  latjjdir  15396  sylow1lem1  16221  sylow1lem5  16225  efgred2  16374  abladdsub4  16427  ablpnpcan  16433  ghmplusg  16452  frgpnabllem2  16476  isabvd  17031  lmodvs1  17102  lspsolvlem  17349  evlslem1  17728  frgpcyg  18134  ip2di  18198  mdetuni0  18562  elptr2  19282  qtophmeo  19525  blss2ps  20113  blss2  20114  blssps  20134  blss  20135  xmeter  20143  metdcnlem  20548  lebnumii  20673  minveclem2  21048  pjthlem1  21059  volfiniun  21164  dvfsumrlimge0  21638  lgsdi  22807  ax5seglem3  23349  ax5seglem6  23352  axcontlem8  23389  gxdi  23955  vacn  24261  minvecolem2  24448  minvecolem4  24453  disjabrex  26097  disjabrexf  26098  slmdvs1  26401  slmd0vs  26405  ornglmulle  26438  orngrmulle  26439  orngmullt  26442  prodmolem2a  27611  cgrcomand  28186  cgrcomr  28192  cgrcomland  28194  cgrcomrand  28195  cgrtriv  28197  cgrid2  28198  ofscom  28202  cgrextend  28203  segconeq  28205  btwntriv2  28207  btwnexch3and  28216  btwnouttr2  28217  btwnouttr  28219  btwnexch  28220  btwnexchand  28221  btwndiff  28222  ifscgr  28239  cgrsub  28240  cgrxfr  28250  lineext  28271  endofsegid  28280  btwnconn1lem2  28283  btwnconn1lem3  28284  btwnconn1lem4  28285  btwnconn1lem5  28286  btwnconn1lem7  28288  btwnconn1lem8  28289  btwnconn1lem10  28291  btwnconn1lem11  28292  btwnconn1lem13  28294  btwnconn1lem14  28295  btwnconn3  28298  midofsegid  28299  segcon2  28300  brsegle2  28304  seglecgr12im  28305  seglecgr12  28306  seglerflx  28307  seglemin  28308  segletr  28309  btwnsegle  28312  colinbtwnle  28313  btwnoutside  28320  broutsideof3  28321  outsideoftr  28324  outsideofeq  28325  outsidele  28327  lineunray  28342  lineelsb2  28343  pellfundex  29395  rmxypairf1o  29420  rmxycomplete  29426  rmxyneg  29429  rmxyadd  29430  rmxy1  29431  rmxy0  29432  jm2.22  29512  proot1mul  29732  deg1mhm  29743  stoweidlem7  29970  stoweidlem36  29999  cpmadugsumlemB  31380  lfladdcl  33074  lshpkrlem4  33116  latmmdiN  33237  latmmdir  33238  hlatj4  33376  4atlem4b  33602  4atlem11  33611  4atlem12  33614  dalem2  33663  dalem-cly  33673  dalem10  33675  dalem23  33698  dalem38  33712  dalem44  33718  dalem55  33729  cdlema1N  33793  paddclN  33844  pmapjoin  33854  dalawlem3  33875  dalawlem5  33877  dalawlem7  33879  dalawlem8  33880  dalawlem11  33883  dalawlem12  33884  lhpexle3lem  34013  4atexlemc  34071  trlnidat  34175  arglem1N  34192  cdlemd9  34208  cdleme0moN  34227  cdleme11c  34263  cdleme11h  34268  cdleme11  34272  cdleme16c  34282  cdleme16f  34285  cdlemeda  34300  cdleme20l2  34323  cdlemefs32sn1aw  34416  cdleme43fsv1snlem  34422  cdleme41sn3a  34435  cdleme32fva  34439  cdleme32b  34444  cdleme32c  34445  cdleme32e  34447  cdleme40m  34469  cdleme40n  34470  cdleme42e  34481  cdleme48d  34537  cdlemf2  34564  cdlemf  34565  cdlemg2fv2  34602  cdlemg7fvbwN  34609  cdlemg7fvN  34626  cdlemg9a  34634  cdlemg9b  34635  cdlemg10a  34642  cdlemg12b  34646  cdlemg17b  34664  cdlemg31d  34702  cdlemg33b0  34703  cdlemg33a  34708  ltrnco  34721  ltrncom  34740  cdlemh  34819  cdlemk3  34835  cdlemk12  34852  cdlemk12u  34874  cdlemkfid1N  34923  cdlemk51  34955  cdlemk54  34960  cdlemk43N  34965  cdlemk35u  34966  cdlemk55u1  34967  cdlemk39u1  34969  cdlemk19u1  34971  dia2dimlem10  35076  dvhgrp  35110  dvh0g  35114  cdlemm10N  35121  diblsmopel  35174  cdlemn4  35201  cdlemn6  35205  cdlemn7  35206  dihordlem7  35217  dihord1  35221  dihord2pre  35228  dihvalcqat  35242  dihopelvalcpre  35251  dihord5apre  35265  dihord  35267  dih1  35289  dihglbcpreN  35303  dihjatc1  35314  dihmeetlem13N  35322  dihmeetALTN  35330  dihjatcclem1  35421  baerlem3lem1  35710
  Copyright terms: Public domain W3C validator