Theorem syl32anc 1378

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 512	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl32anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl31anc 1373	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  coftr  10264  fin1a2s  10405  ioounsn  13450  snunioo  13451  snunico  13452  snunioc  13453  exple1  14137  leexp2rd  14214  facubnd  14256  permnn  14282  sqgcd  16498  cncongr2  16601  hashgcdlem  16717  ramlb  16948  0ram  16949  ram0  16951  ramz2  16953  ramz  16954  ramcl  16958  lsmub1x  19508  lsmub2x  19509  lsmsubm  19515  pgpfac1lem2  19939  mptscmfsupp0  20529  xrsdsreclblem  20983  uvcff  21337  uvcresum  21339  frlmup1  21344  psrass1lemOLD  21484  psrass1lem  21487  psrlidm  21514  psrridm  21515  psrcom  21520  mvrcl  21542  mplsubrglem  21554  mplcoe5  21586  mplbas2  21588  psrbagev1  21629  psrbagev1OLD  21630  evlslem3  21634  evlslem6  21635  psropprmul  21751  smadiadetg  22166  cayhamlem4  22381  lecldbas  22714  pnfnei  22715  mnfnei  22716  clsconn  22925  txcls  23099  ufldom  23457  hauspwpwf1  23482  flfcnp  23499  flfcnp2  23502  cnpfcfi  23535  tsmsmhm  23641  met2ndci  24022  nghmco  24246  nghmplusg  24248  icopnfcld  24275  iocmnfcld  24276  tgioo  24303  reconnlem1  24333  metdseq0  24361  ovolunnul  25008  volinun  25054  volfiniun  25055  volsup  25064  icombl  25072  ioombl  25073  ovolioo  25076  ioorcl2  25080  volivth  25115  ismbf3d  25162  dvferm2lem  25494  lhop  25524  tayl0  25865  pserulm  25925  cxpcn3  26245  ssscongptld  26316  heron  26332  dvdsmulf1o  26687  logexprlim  26717  perfectlem2  26722  lgssq  26829  lgssq2  26830  gausslemma2dlem7  26865  lgsquad2lem1  26876  lgsquad2lem2  26877  2sqblem  26923  addsq2nreurex  26936  ostth2lem2  27126  ostth3  27130  ubthlem2  30111  nmopleid  31379  fsuppcurry1  31937  fsuppcurry2  31938  prmdvdsbc  32009  numdenneg  32010  mgcf1olem1  32158  mgcf1olem2  32159  gsummptres2  32192  archirngz  32322  archiabllem1a  32324  evls1fpws  32634  ply1degltdimlem  32695  fedgmullem1  32702  fedgmullem2  32703  submatminr1  32778  locfinreflem  32808  sxbrsigalem2  33273  elmrsubrn  34499  ismblfin  36517  itg2gt0cn  36531  cntotbnd  36652  ismtyhmeolem  36660  heibor1lem  36665  heiborlem6  36672  rrnequiv  36691  1cvrat  38335  ps-2b  38341  2at0mat0  38384  ps-2c  38387  llncvrlpln2  38416  2llnmeqat  38430  4atlem10  38465  4atlem11a  38466  4atlem12a  38469  2lplnja  38478  dalemcea  38519  dalem2  38520  dalem21  38553  dalem54  38585  2lnat  38643  cdlemb  38653  elpaddat  38663  paddasslem7  38685  paddasslem9  38687  paddasslem10  38688  paddasslem15  38693  poml6N  38814  osumcllem6N  38820  osumcllem7N  38821  pexmidlem4N  38832  pl42lem4N  38841  lhplt  38859  lhpjat1  38879  cdlemc5  39054  cdlemeg46fgN  39393  cdlemg12g  39508  tendoco2  39627  tendococl  39631  tendodi1  39643  tendoicl  39655  cdlemi2  39678  tendospdi1  39879  dihord11c  40083  dihmeetlem6  40168  dihjatc1  40170  dihmeetlem10N  40175  fsuppsssuppgd  41061  expgcd  41220  fltnltalem  41400  jm2.20nn  41721  kercvrlsm  41810  omord2lim  42035  frege96d  42485  frege98d  42489  ntrclsk3  42806  snunioo1  44211  limcleqr  44346  dvdivbd  44625  volioc  44674  iblspltprt  44675  volico  44685  stoweidlem1  44703  stoweidlem24  44726  etransclem23  44959  iccpartipre  46075  2pwp1prm  46243  perfectALTVlem2  46376  2idlcpblrng  46747  lincresunit2  47112  expnegico01  47152  itscnhlinecirc02plem3  47423