Theorem syl32anc 1405

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  fsuppsssuppgd  9374  coftr  10351  fin1a2s  10492  ioounsn  13608  snunioo  13609  snunico  13610  snunioc  13611  leexp1ad  14319  exple1  14320  leexp2rd  14399  facubnd  14444  permnn  14470  sqgcd  16736  expgcd  16737  cncongr2  16843  prmdvdsbc  16902  hashgcdlem  16965  ramlb  17197  0ram  17198  ram0  17200  ramz2  17202  ramz  17203  ramcl  17207  lsmub1x  19860  lsmub2x  19861  lsmsubm  19867  pgpfac1lem2  20291  mptscmfsupp0  21202  2idlcpblrng  21565  xrsdsreclblem  21719  pzriprnglem12  21798  uvcff  22097  uvcresum  22099  frlmup1  22104  psrass1lem  22241  psrlidm  22269  psrridm  22270  psrcom  22275  mvrcl  22299  mplsubrglem  22311  mplcoe5  22349  mplbas2  22351  psrbagev1  22386  evlslem3  22389  evlslem6  22390  psropprmul  22555  evls1fpws  22687  smadiadetg  22988  cayhamlem4  23206  lecldbas  23537  pnfnei  23538  mnfnei  23539  clsconn  23748  txcls  23923  ufldom  24281  hauspwpwf1  24306  flfcnp  24323  flfcnp2  24326  cnpfcfi  24359  tsmsmhm  24465  met2ndci  24841  nghmco  25057  nghmplusg  25059  icopnfcld  25086  iocmnfcld  25087  tgioo  25115  reconnlem1  25146  metdseq0  25174  ovolunnul  25821  volinun  25867  volfiniun  25868  volsup  25877  icombl  25885  ioombl  25886  ovolioo  25889  ioorcl2  25893  volivth  25928  ismbf3d  25975  dvferm2lem  26306  lhop  26336  tayl0  26689  pserulm  26749  cxpcn3  27076  ssscongptld  27150  heron  27166  mpodvdsmulf1o  27521  dvdsmulf1o  27523  logexprlim  27552  perfectlem2  27557  lgssq  27664  lgssq2  27665  gausslemma2dlem7  27700  lgsquad2lem1  27711  lgsquad2lem2  27712  2sqblem  27758  addsq2nreurex  27771  ostth2lem2  27961  ostth3  27965  bdayfinbndlem1  28853  ubthlem2  31473  nmopleid  32741  elsuppfnd  33275  fsuppcurry1  33316  fsuppcurry2  33317  znumd  33404  zdend  33405  numdenneg  33406  mgcf1olem1  33562  mgcf1olem2  33563  gsummptres2  33614  archirngz  33750  archiabllem1a  33752  elrgspnlem2  33804  elrgspnlem3  33805  q1pdir  34135  q1pvsca  34136  ply1degltdimlem  34254  fedgmullem1  34261  fedgmullem2  34262  evls1fldgencl  34302  cos9thpiminplylem1  34414  cos9thpiminplylem2  34415  submatminr1  34442  locfinreflem  34472  sxbrsigalem2  34918  elmrsubrn  36285  ismblfin  38580  itg2gt0cn  38594  cntotbnd  38731  ismtyhmeolem  38739  heibor1lem  38744  heiborlem6  38751  rrnequiv  38770  1cvrat  40534  ps-2b  40540  2at0mat0  40583  ps-2c  40586  llncvrlpln2  40615  2llnmeqat  40629  4atlem10  40664  4atlem11a  40665  4atlem12a  40668  2lplnja  40677  dalemcea  40718  dalem2  40719  dalem21  40752  dalem54  40784  2lnat  40842  cdlemb  40852  elpaddat  40862  paddasslem7  40884  paddasslem9  40886  paddasslem10  40887  paddasslem15  40892  poml6N  41013  osumcllem6N  41019  osumcllem7N  41020  pexmidlem4N  41031  pl42lem4N  41040  lhplt  41058  lhpjat1  41078  cdlemc5  41253  cdlemeg46fgN  41592  cdlemg12g  41707  tendoco2  41826  tendococl  41830  tendodi1  41842  tendoicl  41854  cdlemi2  41877  tendospdi1  42078  dihord11c  42282  dihmeetlem6  42367  dihjatc1  42369  dihmeetlem10N  42374  fltnltalem  43674  jm2.20nn  44004  kercvrlsm  44085  omord2lim  44302  frege96d  44749  frege98d  44753  ntrclsk3  45070  snunioo1  46524  limcleqr  46654  dvdivbd  46933  volioc  46982  iblspltprt  46983  volico  46993  stoweidlem1  47011  stoweidlem24  47034  etransclem23  47267  submodlt  48426  iccpartipre  48503  2pwp1prm  48674  perfectALTVlem2  48820  lincresunit2  49590  expnegico01  49630  itscnhlinecirc02plem3  49896