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

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

Proof of Theorem syl32anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 554 . 2 (𝜑 → (𝜏𝜂))
7 syl32anc.6 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl31anc 1326 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  coftr  9039  fin1a2s  9180  snunioo  12240  snunico  12241  snunioc  12242  exple1  12860  leexp2rd  12982  facubnd  13027  permnn  13053  reuccats1  13418  dvdsadd2b  14952  dvdsmulgcd  15198  sqgcd  15202  bezoutr  15205  cncongr2  15306  hashgcdlem  15417  ramlb  15647  0ram  15648  ram0  15650  ramz2  15652  ramz  15653  ramcl  15657  lsmub1x  17982  lsmub2x  17983  lsmsubm  17989  pgpfac1lem2  18395  mptscmfsupp0  18849  psrass1lem  19296  psrlidm  19322  psrridm  19323  psrcom  19328  mplsubrglem  19358  mvrcl  19368  mplcoe5  19387  mplbas2  19389  psrbagev1  19429  evlslem6  19432  evlslem3  19433  psropprmul  19527  xrsdsreclblem  19711  uvcff  20049  uvcresum  20051  frlmup1  20056  smadiadetg  20398  cayhamlem4  20612  lecldbas  20933  pnfnei  20934  mnfnei  20935  clsconn  21143  txcls  21317  ufldom  21676  hauspwpwf1  21701  flfcnp  21718  flfcnp2  21721  cnpfcfi  21754  tsmsmhm  21859  met2ndci  22237  nghmco  22452  nghmplusg  22454  icopnfcld  22481  iocmnfcld  22482  tgioo  22507  reconnlem1  22537  metdseq0  22565  ovolunnul  23175  volinun  23221  volfiniun  23222  volsup  23231  icombl  23239  ioombl  23240  ovolioo  23243  ioorcl2  23246  volivth  23281  ismbf3d  23327  dvferm2lem  23653  lhop  23683  tayl0  24020  pserulm  24080  cxpcn3  24389  ssscongptld  24452  heron  24465  dvdsmulf1o  24820  logexprlim  24850  perfectlem2  24855  lgssq  24962  lgssq2  24963  gausslemma2dlem7  24998  lgsquad2lem1  25009  lgsquad2lem2  25010  2sqblem  25056  ostth2lem2  25223  ostth3  25227  ubthlem2  27576  nmopleid  28847  numdenneg  29404  2sqcoprm  29432  archirngz  29528  archiabllem1a  29530  submatminr1  29658  locfinreflem  29689  sxbrsigalem2  30129  oddpwdc  30197  ballotlemsdom  30354  ballotlemsel1i  30355  ballotlemsima  30358  ballotlemfrcn0  30372  elmrsubrn  31125  ismblfin  33082  itg2gt0cn  33097  cntotbnd  33227  ismtyhmeolem  33235  heibor1lem  33240  heiborlem6  33247  rrnequiv  33266  1cvrat  34242  ps-2b  34248  2at0mat0  34291  ps-2c  34294  llncvrlpln2  34323  2llnmeqat  34337  4atlem10  34372  4atlem11a  34373  4atlem12a  34376  2lplnja  34385  dalemcea  34426  dalem2  34427  dalem21  34460  dalem54  34492  2lnat  34550  cdlemb  34560  elpaddat  34570  paddasslem7  34592  paddasslem9  34594  paddasslem10  34595  paddasslem15  34600  poml6N  34721  osumcllem6N  34727  osumcllem7N  34728  pexmidlem4N  34739  pl42lem4N  34748  lhplt  34766  lhpjat1  34786  cdlemc5  34962  cdlemeg46fgN  35302  cdlemg12g  35417  tendoco2  35536  tendococl  35540  tendodi1  35552  tendoicl  35564  cdlemi2  35587  tendospdi1  35789  dihord11c  35993  dihmeetlem6  36078  dihjatc1  36080  dihmeetlem10N  36085  jm2.20nn  37044  jm2.25  37046  kercvrlsm  37133  frege96d  37522  frege98d  37526  ntrclsk3  37850  binomcxplemnn0  38030  snunioo2  39142  snunioo1  39149  limcleqr  39280  dvdivbd  39444  volioc  39495  iblspltprt  39496  volico  39507  stoweidlem1  39525  stoweidlem20  39544  stoweidlem24  39548  etransclem23  39781  iccpartipre  40655  2pwp1prm  40802  perfectALTVlem2  40926  lincresunit2  41555  expnegico01  41596
  Copyright terms: Public domain W3C validator