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

Theorem syl32anc 1226
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 )
syl32anc.6  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
Assertion
Ref Expression
syl32anc  |-  ( ph  ->  ze )

Proof of Theorem syl32anc
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 syl32anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl31anc 1221 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:  coftr  8434  fin1a2s  8575  snunioo  11403  snunico  11404  snunioc  11405  exple1  11915  leexp2rd  12033  facubnd  12068  permnn  12094  dvdsadd2b  13567  dvdsmulgcd  13730  sqgcd  13734  ramlb  14072  0ram  14073  ram0  14075  ramz2  14077  ramz  14078  ramcl  14082  lsmub1x  16136  lsmub2x  16137  lsmsubm  16143  pgpfac1lem2  16564  mptscmfsuppd  16989  psrass1lem  17424  psrlidm  17451  psrridm  17453  psrdi  17456  psrdir  17457  psrcom  17458  mplsubrglem  17494  mvrcl  17505  mplcoe2  17524  mplbas2  17526  psrbagev1  17569  evlslem6  17573  evlslem3  17575  psropprmul  17668  xrsdsreclblem  17834  uvcff  18191  uvcresum  18193  frlmup1  18201  smadiadetg  18454  lecldbas  18798  pnfnei  18799  mnfnei  18800  clscon  19009  txcls  19152  ufldom  19510  hauspwpwf1  19535  flfcnp  19552  flfcnp2  19555  cnpfcfi  19588  tsmsmhm  19695  met2ndci  20072  nghmco  20292  nghmplusg  20294  icopnfcld  20322  iocmnfcld  20323  tgioo  20348  reconnlem1  20378  metdseq0  20405  ovolunnul  20958  volinun  21002  volfiniun  21003  volsup  21012  icombl  21020  ioombl  21021  ovolioo  21024  ioorcl2  21027  volivth  21062  ismbf3d  21107  dvferm2lem  21433  lhop  21463  tayl0  21802  pserulm  21862  cxpcn3  22161  ssscongptld  22195  heron  22208  dvdsmulf1o  22509  logexprlim  22539  perfectlem2  22544  lgssq  22649  lgssq2  22650  lgsquad2lem1  22672  lgsquad2lem2  22673  2sqblem  22691  ostth2lem2  22858  ostth3  22862  ubthlem2  24223  nmopleid  25494  numdenneg  26037  archirngz  26157  archiabllem1a  26159  sxbrsigalem2  26653  oddpwdc  26689  ballotlemsdom  26846  ballotlemsel1i  26847  ballotlemsima  26850  ballotlemfrcn0  26864  ismblfin  28385  itg2gt0cn  28400  cntotbnd  28648  ismtyhmeolem  28656  heibor1lem  28661  heiborlem6  28668  rrnequiv  28687  bezoutr  29281  jm2.20nn  29299  jm2.25  29301  kercvrlsm  29389  hashgcdlem  29518  stoweidlem1  29749  stoweidlem20  29768  stoweidlem24  29772  reuccats1  30214  pmatcollpw1lem4  30817  lincresunit2  30901  1cvrat  32960  ps-2b  32966  2at0mat0  33009  ps-2c  33012  llncvrlpln2  33041  2llnmeqat  33055  4atlem10  33090  4atlem11a  33091  4atlem12a  33094  2lplnja  33103  dalemcea  33144  dalem2  33145  dalem21  33178  dalem54  33210  2lnat  33268  cdlemb  33278  elpaddat  33288  paddasslem7  33310  paddasslem9  33312  paddasslem10  33313  paddasslem15  33318  poml6N  33439  osumcllem6N  33445  osumcllem7N  33446  pexmidlem4N  33457  pl42lem4N  33466  lhplt  33484  lhpjat1  33504  cdlemc5  33679  cdlemeg46fgN  34018  cdlemg12g  34133  tendoco2  34252  tendococl  34256  tendodi1  34268  tendoicl  34280  cdlemi2  34303  tendospdi1  34505  dihord11c  34709  dihmeetlem6  34794  dihjatc1  34796  dihmeetlem10N  34801
  Copyright terms: Public domain W3C validator