Theorem syl32anc 1380

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  fsuppsssuppgd  9291  coftr  10186  fin1a2s  10327  ioounsn  13398  snunioo  13399  snunico  13400  snunioc  13401  leexp1ad  14101  exple1  14102  leexp2rd  14180  facubnd  14225  permnn  14251  sqgcd  16491  expgcd  16492  cncongr2  16597  prmdvdsbc  16655  hashgcdlem  16717  ramlb  16949  0ram  16950  ram0  16952  ramz2  16954  ramz  16955  ramcl  16959  lsmub1x  19543  lsmub2x  19544  lsmsubm  19550  pgpfac1lem2  19974  mptscmfsupp0  20848  2idlcpblrng  21196  xrsdsreclblem  21337  pzriprnglem12  21417  uvcff  21716  uvcresum  21718  frlmup1  21723  psrass1lem  21857  psrlidm  21887  psrridm  21888  psrcom  21893  mvrcl  21917  mplsubrglem  21929  mplcoe5  21963  mplbas2  21965  psrbagev1  22000  evlslem3  22003  evlslem6  22004  psropprmul  22138  evls1fpws  22272  smadiadetg  22576  cayhamlem4  22791  lecldbas  23122  pnfnei  23123  mnfnei  23124  clsconn  23333  txcls  23507  ufldom  23865  hauspwpwf1  23890  flfcnp  23907  flfcnp2  23910  cnpfcfi  23943  tsmsmhm  24049  met2ndci  24426  nghmco  24642  nghmplusg  24644  icopnfcld  24671  iocmnfcld  24672  tgioo  24700  reconnlem1  24731  metdseq0  24759  ovolunnul  25417  volinun  25463  volfiniun  25464  volsup  25473  icombl  25481  ioombl  25482  ovolioo  25485  ioorcl2  25489  volivth  25524  ismbf3d  25571  dvferm2lem  25906  lhop  25937  tayl0  26285  pserulm  26347  cxpcn3  26674  ssscongptld  26748  heron  26764  mpodvdsmulf1o  27120  dvdsmulf1o  27122  logexprlim  27152  perfectlem2  27157  lgssq  27264  lgssq2  27265  gausslemma2dlem7  27300  lgsquad2lem1  27311  lgsquad2lem2  27312  2sqblem  27358  addsq2nreurex  27371  ostth2lem2  27561  ostth3  27565  ubthlem2  30833  nmopleid  32101  elsuppfnd  32638  fsuppcurry1  32681  fsuppcurry2  32682  znumd  32770  zdend  32771  numdenneg  32772  mgcf1olem1  32956  mgcf1olem2  32957  gsummptres2  33019  archirngz  33141  archiabllem1a  33143  elrgspnlem2  33193  elrgspnlem3  33194  q1pdir  33544  q1pvsca  33545  ply1degltdimlem  33594  fedgmullem1  33601  fedgmullem2  33602  evls1fldgencl  33641  cos9thpiminplylem1  33748  cos9thpiminplylem2  33749  submatminr1  33776  locfinreflem  33806  sxbrsigalem2  34253  elmrsubrn  35492  ismblfin  37640  itg2gt0cn  37654  cntotbnd  37775  ismtyhmeolem  37783  heibor1lem  37788  heiborlem6  37795  rrnequiv  37814  1cvrat  39455  ps-2b  39461  2at0mat0  39504  ps-2c  39507  llncvrlpln2  39536  2llnmeqat  39550  4atlem10  39585  4atlem11a  39586  4atlem12a  39589  2lplnja  39598  dalemcea  39639  dalem2  39640  dalem21  39673  dalem54  39705  2lnat  39763  cdlemb  39773  elpaddat  39783  paddasslem7  39805  paddasslem9  39807  paddasslem10  39808  paddasslem15  39813  poml6N  39934  osumcllem6N  39940  osumcllem7N  39941  pexmidlem4N  39952  pl42lem4N  39961  lhplt  39979  lhpjat1  39999  cdlemc5  40174  cdlemeg46fgN  40513  cdlemg12g  40628  tendoco2  40747  tendococl  40751  tendodi1  40763  tendoicl  40775  cdlemi2  40798  tendospdi1  40999  dihord11c  41203  dihmeetlem6  41288  dihjatc1  41290  dihmeetlem10N  41295  fltnltalem  42635  jm2.20nn  42970  kercvrlsm  43056  omord2lim  43273  frege96d  43722  frege98d  43726  ntrclsk3  44043  snunioo1  45494  limcleqr  45626  dvdivbd  45905  volioc  45954  iblspltprt  45955  volico  45965  stoweidlem1  45983  stoweidlem24  46006  etransclem23  46239  submodlt  47335  iccpartipre  47406  2pwp1prm  47574  perfectALTVlem2  47707  lincresunit2  48451  expnegico01  48491  itscnhlinecirc02plem3  48757