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

Theorem syl32anc 1375
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 515 . 2 (𝜑 → (𝜏𝜂))
7 syl32anc.6 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl31anc 1370 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  coftr  9684  fin1a2s  9825  ioounsn  12855  snunioo  12856  snunico  12857  snunioc  12858  exple1  13536  leexp2rd  13614  facubnd  13656  permnn  13682  dvdsadd2b  15647  dvdsmulgcd  15894  sqgcd  15898  bezoutr  15901  cncongr2  16001  hashgcdlem  16114  ramlb  16344  0ram  16345  ram0  16347  ramz2  16349  ramz  16350  ramcl  16354  lsmub1x  18762  lsmub2x  18763  lsmsubm  18769  pgpfac1lem2  19188  mptscmfsupp0  19690  xrsdsreclblem  20135  uvcff  20478  uvcresum  20480  frlmup1  20485  psrass1lem  20613  psrlidm  20639  psrridm  20640  psrcom  20645  mplsubrglem  20675  mvrcl  20686  mplcoe5  20706  mplbas2  20708  psrbagev1  20747  evlslem3  20750  evlslem6  20751  psropprmul  20865  smadiadetg  21276  cayhamlem4  21491  lecldbas  21822  pnfnei  21823  mnfnei  21824  clsconn  22033  txcls  22207  ufldom  22565  hauspwpwf1  22590  flfcnp  22607  flfcnp2  22610  cnpfcfi  22643  tsmsmhm  22749  met2ndci  23127  nghmco  23342  nghmplusg  23344  icopnfcld  23371  iocmnfcld  23372  tgioo  23399  reconnlem1  23429  metdseq0  23457  ovolunnul  24102  volinun  24148  volfiniun  24149  volsup  24158  icombl  24166  ioombl  24167  ovolioo  24170  ioorcl2  24174  volivth  24209  ismbf3d  24256  dvferm2lem  24587  lhop  24617  tayl0  24955  pserulm  25015  cxpcn3  25335  ssscongptld  25406  heron  25422  dvdsmulf1o  25777  logexprlim  25807  perfectlem2  25812  lgssq  25919  lgssq2  25920  gausslemma2dlem7  25955  lgsquad2lem1  25966  lgsquad2lem2  25967  2sqblem  26013  2sqcoprm  26017  addsq2nreurex  26026  ostth2lem2  26216  ostth3  26220  ubthlem2  28652  nmopleid  29920  fsuppcurry1  30471  fsuppcurry2  30472  prmdvdsbc  30542  numdenneg  30543  pfxlsw2ccat  30636  wrdt2ind  30637  cyc3conja  30830  archirngz  30849  archiabllem1a  30851  fedgmullem1  31082  fedgmullem2  31083  submatminr1  31132  locfinreflem  31162  sxbrsigalem2  31618  oddpwdc  31686  ballotlemsdom  31843  ballotlemsel1i  31844  ballotlemsima  31847  ballotlemfrcn0  31861  fsum2dsub  31952  circlemeth  31985  elmrsubrn  32841  ismblfin  35056  itg2gt0cn  35070  cntotbnd  35192  ismtyhmeolem  35200  heibor1lem  35205  heiborlem6  35212  rrnequiv  35231  1cvrat  36730  ps-2b  36736  2at0mat0  36779  ps-2c  36782  llncvrlpln2  36811  2llnmeqat  36825  4atlem10  36860  4atlem11a  36861  4atlem12a  36864  2lplnja  36873  dalemcea  36914  dalem2  36915  dalem21  36948  dalem54  36980  2lnat  37038  cdlemb  37048  elpaddat  37058  paddasslem7  37080  paddasslem9  37082  paddasslem10  37083  paddasslem15  37088  poml6N  37209  osumcllem6N  37215  osumcllem7N  37216  pexmidlem4N  37227  pl42lem4N  37236  lhplt  37254  lhpjat1  37274  cdlemc5  37449  cdlemeg46fgN  37788  cdlemg12g  37903  tendoco2  38022  tendococl  38026  tendodi1  38038  tendoicl  38050  cdlemi2  38073  tendospdi1  38274  dihord11c  38478  dihmeetlem6  38563  dihjatc1  38565  dihmeetlem10N  38570  prodsplit  39336  expgcd  39435  fltnltalem  39548  jm2.20nn  39868  jm2.25  39870  kercvrlsm  39957  frege96d  40380  frege98d  40384  ntrclsk3  40706  binomcxplemnn0  40987  snunioo1  42088  limcleqr  42225  dvdivbd  42504  volioc  42553  iblspltprt  42554  volico  42564  stoweidlem1  42582  stoweidlem20  42601  stoweidlem24  42605  etransclem23  42838  iccpartipre  43877  2pwp1prm  44045  perfectALTVlem2  44179  lincresunit2  44826  expnegico01  44866  itscnhlinecirc02plem3  45137
  Copyright terms: Public domain W3C validator