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

Theorem syl122anc 1235
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 530 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl122anc.6 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl121anc 1231 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  divdiv32d  10280  divcan5d  10281  divcan7d  10283  divdiv1d  10286  divdiv2d  10287  seqcoll  12435  cau3lem  13208  eqsqrtd  13221  isercolllem2  13509  isercoll  13511  summolem2a  13558  divrcnv  13685  prodmolem2a  13762  prmind2  14249  divnumden  14302  pceulem  14390  pcqmul  14398  pcqdiv  14402  pcexp  14404  pcaddlem  14428  pcbc  14440  latledi  15855  latjjdi  15869  latjjdir  15870  sylow1lem1  16754  sylow1lem5  16758  efgred2  16907  abladdsub4  16960  ablpnpcan  16966  ghmplusg  16988  frgpnabllem2  17014  isabvd  17601  lmodvs1  17672  lspsolvlem  17920  evlslem1  18316  frgpcyg  18722  ip2di  18786  mdetuni0  19227  cpmadugsumlemB  19479  elptr2  20179  blss2ps  21010  blss2  21011  blssps  21031  blss  21032  xmeter  21040  metdcnlem  21445  lebnumii  21570  minveclem2  21945  pjthlem1  21956  volfiniun  22061  dvfsumrlimge0  22535  lgsdi  23743  ax5seglem3  24376  ax5seglem6  24379  axcontlem8  24416  eengtrkg  24430  gxdi  25436  vacn  25742  minvecolem2  25929  minvecolem4  25934  disjabrex  27601  disjabrexf  27602  slmdvs1  27946  slmd0vs  27950  orngsqr  27979  ornglmulle  27980  orngrmulle  27981  orngmullt  27984  suborng  27990  cgrcomand  29830  cgrcomr  29836  cgrcomland  29838  cgrcomrand  29839  cgrtriv  29841  cgrid2  29842  ofscom  29846  cgrextend  29847  segconeq  29849  btwntriv2  29851  btwnexch3and  29860  btwnouttr2  29861  btwnouttr  29863  btwnexch  29864  btwnexchand  29865  btwndiff  29866  ifscgr  29883  cgrsub  29884  cgrxfr  29894  lineext  29915  endofsegid  29924  btwnconn1lem2  29927  btwnconn1lem3  29928  btwnconn1lem4  29929  btwnconn1lem5  29930  btwnconn1lem7  29932  btwnconn1lem8  29933  btwnconn1lem10  29935  btwnconn1lem11  29936  btwnconn1lem13  29938  btwnconn1lem14  29939  btwnconn3  29942  midofsegid  29943  segcon2  29944  brsegle2  29948  seglecgr12im  29949  seglecgr12  29950  seglerflx  29951  seglemin  29952  segletr  29953  btwnsegle  29956  colinbtwnle  29957  btwnoutside  29964  broutsideof3  29965  outsideoftr  29968  outsideofeq  29969  outsidele  29971  lineunray  29986  lineelsb2  29987  pellfundex  31023  rmxypairf1o  31048  rmxycomplete  31054  rmxyneg  31057  rmxyadd  31058  rmxy1  31059  rmxy0  31060  jm2.22  31139  proot1mul  31360  deg1mhm  31371  stoweidlem7  31990  stoweidlem36  32019  lfladdcl  35244  lshpkrlem4  35286  latmmdiN  35407  latmmdir  35408  hlatj4  35546  4atlem4b  35772  4atlem11  35781  4atlem12  35784  dalem2  35833  dalem-cly  35843  dalem10  35845  dalem23  35868  dalem38  35882  dalem44  35888  dalem55  35899  cdlema1N  35963  paddclN  36014  pmapjoin  36024  dalawlem3  36045  dalawlem5  36047  dalawlem7  36049  dalawlem8  36050  dalawlem11  36053  dalawlem12  36054  lhpexle3lem  36183  4atexlemc  36241  trlnidat  36346  arglem1N  36363  cdlemd9  36379  cdleme0moN  36398  cdleme11c  36434  cdleme11h  36439  cdleme11  36443  cdleme16c  36453  cdleme16f  36456  cdlemeda  36471  cdleme20l2  36495  cdlemefs32sn1aw  36588  cdleme43fsv1snlem  36594  cdleme41sn3a  36607  cdleme32fva  36611  cdleme32b  36616  cdleme32c  36617  cdleme32e  36619  cdleme40m  36641  cdleme40n  36642  cdleme42e  36653  cdleme48d  36709  cdlemf2  36736  cdlemf  36737  cdlemg2fv2  36774  cdlemg7fvbwN  36781  cdlemg7fvN  36798  cdlemg9a  36806  cdlemg9b  36807  cdlemg10a  36814  cdlemg12b  36818  cdlemg17b  36836  cdlemg31d  36874  cdlemg33b0  36875  cdlemg33a  36880  ltrnco  36893  ltrncom  36912  cdlemh  36991  cdlemk3  37007  cdlemk12  37024  cdlemk12u  37046  cdlemkfid1N  37095  cdlemk51  37127  cdlemk54  37132  cdlemk43N  37137  cdlemk35u  37138  cdlemk55u1  37139  cdlemk39u1  37141  cdlemk19u1  37143  dia2dimlem10  37248  dvhgrp  37282  dvh0g  37286  cdlemm10N  37293  diblsmopel  37346  cdlemn4  37373  cdlemn6  37377  cdlemn7  37378  dihordlem7  37389  dihord1  37393  dihord2pre  37400  dihvalcqat  37414  dihopelvalcpre  37423  dihord5apre  37437  dihord  37439  dih1  37461  dihglbcpreN  37475  dihjatc1  37486  dihmeetlem13N  37494  dihmeetALTN  37502  dihjatcclem1  37593  baerlem3lem1  37882
  Copyright terms: Public domain W3C validator