Theorem syl32anc 1377

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 1372	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  coftr  10038  fin1a2s  10179  ioounsn  13218  snunioo  13219  snunico  13220  snunioc  13221  exple1  13903  leexp2rd  13981  facubnd  14023  permnn  14049  sqgcd  16279  cncongr2  16382  hashgcdlem  16498  ramlb  16729  0ram  16730  ram0  16732  ramz2  16734  ramz  16735  ramcl  16739  lsmub1x  19260  lsmub2x  19261  lsmsubm  19267  pgpfac1lem2  19687  mptscmfsupp0  20197  xrsdsreclblem  20653  uvcff  21007  uvcresum  21009  frlmup1  21014  psrass1lemOLD  21152  psrass1lem  21155  psrlidm  21181  psrridm  21182  psrcom  21187  mplsubrglem  21219  mvrcl  21230  mplcoe5  21250  mplbas2  21252  psrbagev1  21294  psrbagev1OLD  21295  evlslem3  21299  evlslem6  21300  psropprmul  21418  smadiadetg  21831  cayhamlem4  22046  lecldbas  22379  pnfnei  22380  mnfnei  22381  clsconn  22590  txcls  22764  ufldom  23122  hauspwpwf1  23147  flfcnp  23164  flfcnp2  23167  cnpfcfi  23200  tsmsmhm  23306  met2ndci  23687  nghmco  23911  nghmplusg  23913  icopnfcld  23940  iocmnfcld  23941  tgioo  23968  reconnlem1  23998  metdseq0  24026  ovolunnul  24673  volinun  24719  volfiniun  24720  volsup  24729  icombl  24737  ioombl  24738  ovolioo  24741  ioorcl2  24745  volivth  24780  ismbf3d  24827  dvferm2lem  25159  lhop  25189  tayl0  25530  pserulm  25590  cxpcn3  25910  ssscongptld  25981  heron  25997  dvdsmulf1o  26352  logexprlim  26382  perfectlem2  26387  lgssq  26494  lgssq2  26495  gausslemma2dlem7  26530  lgsquad2lem1  26541  lgsquad2lem2  26542  2sqblem  26588  addsq2nreurex  26601  ostth2lem2  26791  ostth3  26795  ubthlem2  29242  nmopleid  30510  fsuppcurry1  31069  fsuppcurry2  31070  prmdvdsbc  31139  numdenneg  31140  mgcf1olem1  31288  mgcf1olem2  31289  gsummptres2  31322  archirngz  31452  archiabllem1a  31454  fedgmullem1  31719  fedgmullem2  31720  submatminr1  31769  locfinreflem  31799  sxbrsigalem2  32262  elmrsubrn  33491  ismblfin  35827  itg2gt0cn  35841  cntotbnd  35963  ismtyhmeolem  35971  heibor1lem  35976  heiborlem6  35983  rrnequiv  36002  1cvrat  37497  ps-2b  37503  2at0mat0  37546  ps-2c  37549  llncvrlpln2  37578  2llnmeqat  37592  4atlem10  37627  4atlem11a  37628  4atlem12a  37631  2lplnja  37640  dalemcea  37681  dalem2  37682  dalem21  37715  dalem54  37747  2lnat  37805  cdlemb  37815  elpaddat  37825  paddasslem7  37847  paddasslem9  37849  paddasslem10  37850  paddasslem15  37855  poml6N  37976  osumcllem6N  37982  osumcllem7N  37983  pexmidlem4N  37994  pl42lem4N  38003  lhplt  38021  lhpjat1  38041  cdlemc5  38216  cdlemeg46fgN  38555  cdlemg12g  38670  tendoco2  38789  tendococl  38793  tendodi1  38805  tendoicl  38817  cdlemi2  38840  tendospdi1  39041  dihord11c  39245  dihmeetlem6  39330  dihjatc1  39332  dihmeetlem10N  39337  expgcd  40341  fltnltalem  40506  jm2.20nn  40826  kercvrlsm  40915  frege96d  41364  frege98d  41368  ntrclsk3  41687  snunioo1  43057  limcleqr  43192  dvdivbd  43471  volioc  43520  iblspltprt  43521  volico  43531  stoweidlem1  43549  stoweidlem24  43572  etransclem23  43805  iccpartipre  44884  2pwp1prm  45052  perfectALTVlem2  45185  lincresunit2  45830  expnegico01  45870  itscnhlinecirc02plem3  46141