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

Theorem syl32anc 1379
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 513 . 2 (𝜑 → (𝜏𝜂))
7 syl32anc.6 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl31anc 1374 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  coftr  10214  fin1a2s  10355  ioounsn  13400  snunioo  13401  snunico  13402  snunioc  13403  exple1  14087  leexp2rd  14164  facubnd  14206  permnn  14232  sqgcd  16446  cncongr2  16549  hashgcdlem  16665  ramlb  16896  0ram  16897  ram0  16899  ramz2  16901  ramz  16902  ramcl  16906  lsmub1x  19433  lsmub2x  19434  lsmsubm  19440  pgpfac1lem2  19859  mptscmfsupp0  20402  xrsdsreclblem  20859  uvcff  21213  uvcresum  21215  frlmup1  21220  psrass1lemOLD  21358  psrass1lem  21361  psrlidm  21388  psrridm  21389  psrcom  21394  mplsubrglem  21426  mvrcl  21437  mplcoe5  21457  mplbas2  21459  psrbagev1  21501  psrbagev1OLD  21502  evlslem3  21506  evlslem6  21507  psropprmul  21625  smadiadetg  22038  cayhamlem4  22253  lecldbas  22586  pnfnei  22587  mnfnei  22588  clsconn  22797  txcls  22971  ufldom  23329  hauspwpwf1  23354  flfcnp  23371  flfcnp2  23374  cnpfcfi  23407  tsmsmhm  23513  met2ndci  23894  nghmco  24118  nghmplusg  24120  icopnfcld  24147  iocmnfcld  24148  tgioo  24175  reconnlem1  24205  metdseq0  24233  ovolunnul  24880  volinun  24926  volfiniun  24927  volsup  24936  icombl  24944  ioombl  24945  ovolioo  24948  ioorcl2  24952  volivth  24987  ismbf3d  25034  dvferm2lem  25366  lhop  25396  tayl0  25737  pserulm  25797  cxpcn3  26117  ssscongptld  26188  heron  26204  dvdsmulf1o  26559  logexprlim  26589  perfectlem2  26594  lgssq  26701  lgssq2  26702  gausslemma2dlem7  26737  lgsquad2lem1  26748  lgsquad2lem2  26749  2sqblem  26795  addsq2nreurex  26808  ostth2lem2  26998  ostth3  27002  ubthlem2  29855  nmopleid  31123  fsuppcurry1  31689  fsuppcurry2  31690  prmdvdsbc  31761  numdenneg  31762  mgcf1olem1  31910  mgcf1olem2  31911  gsummptres2  31944  archirngz  32074  archiabllem1a  32076  evls1fpws  32320  ply1degltdimlem  32374  fedgmullem1  32381  fedgmullem2  32382  submatminr1  32448  locfinreflem  32478  sxbrsigalem2  32943  elmrsubrn  34171  ismblfin  36165  itg2gt0cn  36179  cntotbnd  36301  ismtyhmeolem  36309  heibor1lem  36314  heiborlem6  36321  rrnequiv  36340  1cvrat  37985  ps-2b  37991  2at0mat0  38034  ps-2c  38037  llncvrlpln2  38066  2llnmeqat  38080  4atlem10  38115  4atlem11a  38116  4atlem12a  38119  2lplnja  38128  dalemcea  38169  dalem2  38170  dalem21  38203  dalem54  38235  2lnat  38293  cdlemb  38303  elpaddat  38313  paddasslem7  38335  paddasslem9  38337  paddasslem10  38338  paddasslem15  38343  poml6N  38464  osumcllem6N  38470  osumcllem7N  38471  pexmidlem4N  38482  pl42lem4N  38491  lhplt  38509  lhpjat1  38529  cdlemc5  38704  cdlemeg46fgN  39043  cdlemg12g  39158  tendoco2  39277  tendococl  39281  tendodi1  39293  tendoicl  39305  cdlemi2  39328  tendospdi1  39529  dihord11c  39733  dihmeetlem6  39818  dihjatc1  39820  dihmeetlem10N  39825  expgcd  40863  fltnltalem  41043  jm2.20nn  41364  kercvrlsm  41453  omord2lim  41678  frege96d  42109  frege98d  42113  ntrclsk3  42430  snunioo1  43836  limcleqr  43971  dvdivbd  44250  volioc  44299  iblspltprt  44300  volico  44310  stoweidlem1  44328  stoweidlem24  44351  etransclem23  44584  iccpartipre  45699  2pwp1prm  45867  perfectALTVlem2  46000  lincresunit2  46645  expnegico01  46685  itscnhlinecirc02plem3  46956
  Copyright terms: Public domain W3C validator