Theorem syl32anc 1393

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  fsuppsssuppgd  9318  coftr  10220  fin1a2s  10361  ioounsn  13471  snunioo  13472  snunico  13473  snunioc  13474  leexp1ad  14179  exple1  14180  leexp2rd  14258  facubnd  14303  permnn  14329  sqgcd  16572  expgcd  16573  cncongr2  16678  prmdvdsbc  16737  hashgcdlem  16799  ramlb  17031  0ram  17032  ram0  17034  ramz2  17036  ramz  17037  ramcl  17041  lsmub1x  19662  lsmub2x  19663  lsmsubm  19669  pgpfac1lem2  20093  mptscmfsupp0  20967  2idlcpblrng  21314  xrsdsreclblem  21438  pzriprnglem12  21517  uvcff  21816  uvcresum  21818  frlmup1  21823  psrass1lem  21958  psrlidm  21986  psrridm  21987  psrcom  21992  mvrcl  22016  mplsubrglem  22028  mplcoe5  22066  mplbas2  22068  psrbagev1  22103  evlslem3  22106  evlslem6  22107  psropprmul  22272  evls1fpws  22405  smadiadetg  22706  cayhamlem4  22921  lecldbas  23252  pnfnei  23253  mnfnei  23254  clsconn  23463  txcls  23637  ufldom  23995  hauspwpwf1  24020  flfcnp  24037  flfcnp2  24040  cnpfcfi  24073  tsmsmhm  24179  met2ndci  24555  nghmco  24771  nghmplusg  24773  icopnfcld  24800  iocmnfcld  24801  tgioo  24829  reconnlem1  24860  metdseq0  24888  ovolunnul  25535  volinun  25581  volfiniun  25582  volsup  25591  icombl  25599  ioombl  25600  ovolioo  25603  ioorcl2  25607  volivth  25642  ismbf3d  25689  dvferm2lem  26021  lhop  26051  tayl0  26395  pserulm  26455  cxpcn3  26783  ssscongptld  26857  heron  26873  mpodvdsmulf1o  27228  dvdsmulf1o  27230  logexprlim  27259  perfectlem2  27264  lgssq  27371  lgssq2  27372  gausslemma2dlem7  27407  lgsquad2lem1  27418  lgsquad2lem2  27419  2sqblem  27465  addsq2nreurex  27478  ostth2lem2  27668  ostth3  27672  bdayfinbndlem1  28530  ubthlem2  31013  nmopleid  32281  elsuppfnd  32827  fsuppcurry1  32869  fsuppcurry2  32870  znumd  32958  zdend  32959  numdenneg  32960  mgcf1olem1  33133  mgcf1olem2  33134  gsummptres2  33187  archirngz  33323  archiabllem1a  33325  elrgspnlem2  33378  elrgspnlem3  33379  q1pdir  33753  q1pvsca  33754  ply1degltdimlem  33873  fedgmullem1  33880  fedgmullem2  33881  evls1fldgencl  33921  cos9thpiminplylem1  34033  cos9thpiminplylem2  34034  submatminr1  34061  locfinreflem  34091  sxbrsigalem2  34537  elmrsubrn  35818  ismblfin  38108  itg2gt0cn  38122  cntotbnd  38243  ismtyhmeolem  38251  heibor1lem  38256  heiborlem6  38263  rrnequiv  38282  1cvrat  40048  ps-2b  40054  2at0mat0  40097  ps-2c  40100  llncvrlpln2  40129  2llnmeqat  40143  4atlem10  40178  4atlem11a  40179  4atlem12a  40182  2lplnja  40191  dalemcea  40232  dalem2  40233  dalem21  40266  dalem54  40298  2lnat  40356  cdlemb  40366  elpaddat  40376  paddasslem7  40398  paddasslem9  40400  paddasslem10  40401  paddasslem15  40406  poml6N  40527  osumcllem6N  40533  osumcllem7N  40534  pexmidlem4N  40545  pl42lem4N  40554  lhplt  40572  lhpjat1  40592  cdlemc5  40767  cdlemeg46fgN  41106  cdlemg12g  41221  tendoco2  41340  tendococl  41344  tendodi1  41356  tendoicl  41368  cdlemi2  41391  tendospdi1  41592  dihord11c  41796  dihmeetlem6  41881  dihjatc1  41883  dihmeetlem10N  41888  fltnltalem  43192  jm2.20nn  43522  kercvrlsm  43608  omord2lim  43825  frege96d  44273  frege98d  44277  ntrclsk3  44594  snunioo1  46036  limcleqr  46166  dvdivbd  46445  volioc  46494  iblspltprt  46495  volico  46505  stoweidlem1  46523  stoweidlem24  46546  etransclem23  46779  submodlt  47898  iccpartipre  47975  2pwp1prm  48146  perfectALTVlem2  48292  lincresunit2  49048  expnegico01  49088  itscnhlinecirc02plem3  49354