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

Theorem syl32anc 1370
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl32anc.6 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
Assertion
Ref Expression
syl32anc (𝜑𝜁)

Proof of Theorem syl32anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 512 . 2 (𝜑 → (𝜏𝜂))
7 syl32anc.6 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl31anc 1365 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  coftr  9683  fin1a2s  9824  ioounsn  12851  snunioo  12852  snunico  12853  snunioc  12854  exple1  13528  leexp2rd  13606  facubnd  13648  permnn  13674  dvdsadd2b  15644  dvdsmulgcd  15893  sqgcd  15897  bezoutr  15900  cncongr2  16000  hashgcdlem  16113  ramlb  16343  0ram  16344  ram0  16346  ramz2  16348  ramz  16349  ramcl  16353  lsmub1x  18700  lsmub2x  18701  lsmsubm  18707  pgpfac1lem2  19126  mptscmfsupp0  19628  psrass1lem  20085  psrlidm  20111  psrridm  20112  psrcom  20117  mplsubrglem  20147  mvrcl  20157  mplcoe5  20177  mplbas2  20179  psrbagev1  20218  evlslem3  20221  evlslem6  20222  psropprmul  20334  xrsdsreclblem  20519  uvcff  20863  uvcresum  20865  frlmup1  20870  smadiadetg  21210  cayhamlem4  21424  lecldbas  21755  pnfnei  21756  mnfnei  21757  clsconn  21966  txcls  22140  ufldom  22498  hauspwpwf1  22523  flfcnp  22540  flfcnp2  22543  cnpfcfi  22576  tsmsmhm  22681  met2ndci  23059  nghmco  23274  nghmplusg  23276  icopnfcld  23303  iocmnfcld  23304  tgioo  23331  reconnlem1  23361  metdseq0  23389  ovolunnul  24028  volinun  24074  volfiniun  24075  volsup  24084  icombl  24092  ioombl  24093  ovolioo  24096  ioorcl2  24100  volivth  24135  ismbf3d  24182  dvferm2lem  24510  lhop  24540  tayl0  24877  pserulm  24937  cxpcn3  25256  ssscongptld  25327  heron  25343  dvdsmulf1o  25698  logexprlim  25728  perfectlem2  25733  lgssq  25840  lgssq2  25841  gausslemma2dlem7  25876  lgsquad2lem1  25887  lgsquad2lem2  25888  2sqblem  25934  2sqcoprm  25938  addsq2nreurex  25947  ostth2lem2  26137  ostth3  26141  ubthlem2  28575  nmopleid  29843  fsuppcurry1  30387  fsuppcurry2  30388  prmdvdsbc  30458  numdenneg  30459  pfxlsw2ccat  30553  wrdt2ind  30554  cyc3conja  30726  archirngz  30745  archiabllem1a  30747  fedgmullem1  30924  fedgmullem2  30925  submatminr1  30974  locfinreflem  31003  sxbrsigalem2  31443  oddpwdc  31511  ballotlemsdom  31668  ballotlemsel1i  31669  ballotlemsima  31672  ballotlemfrcn0  31686  fsum2dsub  31777  circlemeth  31810  elmrsubrn  32664  ismblfin  34814  itg2gt0cn  34828  cntotbnd  34955  ismtyhmeolem  34963  heibor1lem  34968  heiborlem6  34975  rrnequiv  34994  1cvrat  36492  ps-2b  36498  2at0mat0  36541  ps-2c  36544  llncvrlpln2  36573  2llnmeqat  36587  4atlem10  36622  4atlem11a  36623  4atlem12a  36626  2lplnja  36635  dalemcea  36676  dalem2  36677  dalem21  36710  dalem54  36742  2lnat  36800  cdlemb  36810  elpaddat  36820  paddasslem7  36842  paddasslem9  36844  paddasslem10  36845  paddasslem15  36850  poml6N  36971  osumcllem6N  36977  osumcllem7N  36978  pexmidlem4N  36989  pl42lem4N  36998  lhplt  37016  lhpjat1  37036  cdlemc5  37211  cdlemeg46fgN  37550  cdlemg12g  37665  tendoco2  37784  tendococl  37788  tendodi1  37800  tendoicl  37812  cdlemi2  37835  tendospdi1  38036  dihord11c  38240  dihmeetlem6  38325  dihjatc1  38327  dihmeetlem10N  38332  expgcd  39061  fltnltalem  39152  jm2.20nn  39472  jm2.25  39474  kercvrlsm  39561  frege96d  39972  frege98d  39976  ntrclsk3  40298  binomcxplemnn0  40558  snunioo1  41664  limcleqr  41801  dvdivbd  42084  volioc  42133  iblspltprt  42134  volico  42145  stoweidlem1  42163  stoweidlem20  42182  stoweidlem24  42186  etransclem23  42419  iccpartipre  43458  2pwp1prm  43628  perfectALTVlem2  43764  lincresunit2  44461  expnegico01  44501  itscnhlinecirc02plem3  44699
  Copyright terms: Public domain W3C validator