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  9340  coftr  10233  fin1a2s  10374  ioounsn  13445  snunioo  13446  snunico  13447  snunioc  13448  leexp1ad  14148  exple1  14149  leexp2rd  14227  facubnd  14272  permnn  14298  sqgcd  16539  expgcd  16540  cncongr2  16645  prmdvdsbc  16703  hashgcdlem  16765  ramlb  16997  0ram  16998  ram0  17000  ramz2  17002  ramz  17003  ramcl  17007  lsmub1x  19583  lsmub2x  19584  lsmsubm  19590  pgpfac1lem2  20014  mptscmfsupp0  20840  2idlcpblrng  21188  xrsdsreclblem  21336  pzriprnglem12  21409  uvcff  21707  uvcresum  21709  frlmup1  21714  psrass1lem  21848  psrlidm  21878  psrridm  21879  psrcom  21884  mvrcl  21908  mplsubrglem  21920  mplcoe5  21954  mplbas2  21956  psrbagev1  21991  evlslem3  21994  evlslem6  21995  psropprmul  22129  evls1fpws  22263  smadiadetg  22567  cayhamlem4  22782  lecldbas  23113  pnfnei  23114  mnfnei  23115  clsconn  23324  txcls  23498  ufldom  23856  hauspwpwf1  23881  flfcnp  23898  flfcnp2  23901  cnpfcfi  23934  tsmsmhm  24040  met2ndci  24417  nghmco  24633  nghmplusg  24635  icopnfcld  24662  iocmnfcld  24663  tgioo  24691  reconnlem1  24722  metdseq0  24750  ovolunnul  25408  volinun  25454  volfiniun  25455  volsup  25464  icombl  25472  ioombl  25473  ovolioo  25476  ioorcl2  25480  volivth  25515  ismbf3d  25562  dvferm2lem  25897  lhop  25928  tayl0  26276  pserulm  26338  cxpcn3  26665  ssscongptld  26739  heron  26755  mpodvdsmulf1o  27111  dvdsmulf1o  27113  logexprlim  27143  perfectlem2  27148  lgssq  27255  lgssq2  27256  gausslemma2dlem7  27291  lgsquad2lem1  27302  lgsquad2lem2  27303  2sqblem  27349  addsq2nreurex  27362  ostth2lem2  27552  ostth3  27556  ubthlem2  30807  nmopleid  32075  elsuppfnd  32612  fsuppcurry1  32655  fsuppcurry2  32656  znumd  32744  zdend  32745  numdenneg  32746  mgcf1olem1  32934  mgcf1olem2  32935  gsummptres2  33000  archirngz  33150  archiabllem1a  33152  elrgspnlem2  33201  elrgspnlem3  33202  q1pdir  33575  q1pvsca  33576  ply1degltdimlem  33625  fedgmullem1  33632  fedgmullem2  33633  evls1fldgencl  33672  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  submatminr1  33807  locfinreflem  33837  sxbrsigalem2  34284  elmrsubrn  35514  ismblfin  37662  itg2gt0cn  37676  cntotbnd  37797  ismtyhmeolem  37805  heibor1lem  37810  heiborlem6  37817  rrnequiv  37836  1cvrat  39477  ps-2b  39483  2at0mat0  39526  ps-2c  39529  llncvrlpln2  39558  2llnmeqat  39572  4atlem10  39607  4atlem11a  39608  4atlem12a  39611  2lplnja  39620  dalemcea  39661  dalem2  39662  dalem21  39695  dalem54  39727  2lnat  39785  cdlemb  39795  elpaddat  39805  paddasslem7  39827  paddasslem9  39829  paddasslem10  39830  paddasslem15  39835  poml6N  39956  osumcllem6N  39962  osumcllem7N  39963  pexmidlem4N  39974  pl42lem4N  39983  lhplt  40001  lhpjat1  40021  cdlemc5  40196  cdlemeg46fgN  40535  cdlemg12g  40650  tendoco2  40769  tendococl  40773  tendodi1  40785  tendoicl  40797  cdlemi2  40820  tendospdi1  41021  dihord11c  41225  dihmeetlem6  41310  dihjatc1  41312  dihmeetlem10N  41317  fltnltalem  42657  jm2.20nn  42993  kercvrlsm  43079  omord2lim  43296  frege96d  43745  frege98d  43749  ntrclsk3  44066  snunioo1  45517  limcleqr  45649  dvdivbd  45928  volioc  45977  iblspltprt  45978  volico  45988  stoweidlem1  46006  stoweidlem24  46029  etransclem23  46262  submodlt  47355  iccpartipre  47426  2pwp1prm  47594  perfectALTVlem2  47727  lincresunit2  48471  expnegico01  48511  itscnhlinecirc02plem3  48777