Theorem syl32anc 1358

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

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 504	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl32anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl31anc 1353	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  coftr  9485  fin1a2s  9626  ioounsn  12672  snunioo  12673  snunico  12674  snunioc  12675  exple1  13348  leexp2rd  13426  facubnd  13468  permnn  13494  reuccats1OLD  13911  dvdsadd2b  15506  dvdsmulgcd  15751  sqgcd  15755  bezoutr  15758  cncongr2  15858  hashgcdlem  15971  ramlb  16201  0ram  16202  ram0  16204  ramz2  16206  ramz  16207  ramcl  16211  lsmub1x  18522  lsmub2x  18523  lsmsubm  18529  pgpfac1lem2  18937  mptscmfsupp0  19411  psrass1lem  19861  psrlidm  19887  psrridm  19888  psrcom  19893  mplsubrglem  19923  mvrcl  19933  mplcoe5  19952  mplbas2  19954  psrbagev1  19993  evlslem6  19996  evlslem3  19997  psropprmul  20099  xrsdsreclblem  20283  uvcff  20627  uvcresum  20629  frlmup1  20634  smadiadetg  20976  cayhamlem4  21190  lecldbas  21521  pnfnei  21522  mnfnei  21523  clsconn  21732  txcls  21906  ufldom  22264  hauspwpwf1  22289  flfcnp  22306  flfcnp2  22309  cnpfcfi  22342  tsmsmhm  22447  met2ndci  22825  nghmco  23040  nghmplusg  23042  icopnfcld  23069  iocmnfcld  23070  tgioo  23097  reconnlem1  23127  metdseq0  23155  ovolunnul  23794  volinun  23840  volfiniun  23841  volsup  23850  icombl  23858  ioombl  23859  ovolioo  23862  ioorcl2  23866  volivth  23901  ismbf3d  23948  dvferm2lem  24276  lhop  24306  tayl0  24643  pserulm  24703  cxpcn3  25020  ssscongptld  25091  heron  25107  dvdsmulf1o  25463  logexprlim  25493  perfectlem2  25498  lgssq  25605  lgssq2  25606  gausslemma2dlem7  25641  lgsquad2lem1  25652  lgsquad2lem2  25653  2sqblem  25699  2sqcoprm  25703  addsq2nreurex  25712  ostth2lem2  25902  ostth3  25906  ubthlem2  28416  nmopleid  29687  fsuppcurry1  30202  fsuppcurry2  30203  prmdvdsbc  30267  numdenneg  30268  archirngz  30440  archiabllem1a  30442  fedgmullem1  30610  fedgmullem2  30611  submatminr1  30674  locfinreflem  30705  sxbrsigalem2  31146  oddpwdc  31214  ballotlemsdom  31372  ballotlemsel1i  31373  ballotlemsima  31376  ballotlemfrcn0  31390  fsum2dsub  31487  circlemeth  31520  elmrsubrn  32227  ismblfin  34322  itg2gt0cn  34336  cntotbnd  34464  ismtyhmeolem  34472  heibor1lem  34477  heiborlem6  34484  rrnequiv  34503  1cvrat  36005  ps-2b  36011  2at0mat0  36054  ps-2c  36057  llncvrlpln2  36086  2llnmeqat  36100  4atlem10  36135  4atlem11a  36136  4atlem12a  36139  2lplnja  36148  dalemcea  36189  dalem2  36190  dalem21  36223  dalem54  36255  2lnat  36313  cdlemb  36323  elpaddat  36333  paddasslem7  36355  paddasslem9  36357  paddasslem10  36358  paddasslem15  36363  poml6N  36484  osumcllem6N  36490  osumcllem7N  36491  pexmidlem4N  36502  pl42lem4N  36511  lhplt  36529  lhpjat1  36549  cdlemc5  36724  cdlemeg46fgN  37063  cdlemg12g  37178  tendoco2  37297  tendococl  37301  tendodi1  37313  tendoicl  37325  cdlemi2  37348  tendospdi1  37549  dihord11c  37753  dihmeetlem6  37838  dihjatc1  37840  dihmeetlem10N  37845  expgcd  38560  fltnltalem  38626  jm2.20nn  38935  jm2.25  38937  kercvrlsm  39024  frege96d  39402  frege98d  39406  ntrclsk3  39728  binomcxplemnn0  40041  snunioo1  41165  limcleqr  41302  dvdivbd  41584  volioc  41633  iblspltprt  41634  volico  41645  stoweidlem1  41663  stoweidlem20  41682  stoweidlem24  41686  etransclem23  41919  iccpartipre  42899  2pwp1prm  43059  perfectALTVlem2  43195  lincresunit2  43840  expnegico01  43881  itscnhlinecirc02plem3  44079