Theorem syl32anc 1374

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

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

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 1085

This theorem is referenced by:  coftr  9697  fin1a2s  9838  ioounsn  12866  snunioo  12867  snunico  12868  snunioc  12869  exple1  13543  leexp2rd  13621  facubnd  13663  permnn  13689  dvdsadd2b  15658  dvdsmulgcd  15907  sqgcd  15911  bezoutr  15914  cncongr2  16014  hashgcdlem  16127  ramlb  16357  0ram  16358  ram0  16360  ramz2  16362  ramz  16363  ramcl  16367  lsmub1x  18773  lsmub2x  18774  lsmsubm  18780  pgpfac1lem2  19199  mptscmfsupp0  19701  psrass1lem  20159  psrlidm  20185  psrridm  20186  psrcom  20191  mplsubrglem  20221  mvrcl  20231  mplcoe5  20251  mplbas2  20253  psrbagev1  20292  evlslem3  20295  evlslem6  20296  psropprmul  20408  xrsdsreclblem  20593  uvcff  20937  uvcresum  20939  frlmup1  20944  smadiadetg  21284  cayhamlem4  21498  lecldbas  21829  pnfnei  21830  mnfnei  21831  clsconn  22040  txcls  22214  ufldom  22572  hauspwpwf1  22597  flfcnp  22614  flfcnp2  22617  cnpfcfi  22650  tsmsmhm  22756  met2ndci  23134  nghmco  23349  nghmplusg  23351  icopnfcld  23378  iocmnfcld  23379  tgioo  23406  reconnlem1  23436  metdseq0  23464  ovolunnul  24103  volinun  24149  volfiniun  24150  volsup  24159  icombl  24167  ioombl  24168  ovolioo  24171  ioorcl2  24175  volivth  24210  ismbf3d  24257  dvferm2lem  24585  lhop  24615  tayl0  24952  pserulm  25012  cxpcn3  25331  ssscongptld  25402  heron  25418  dvdsmulf1o  25773  logexprlim  25803  perfectlem2  25808  lgssq  25915  lgssq2  25916  gausslemma2dlem7  25951  lgsquad2lem1  25962  lgsquad2lem2  25963  2sqblem  26009  2sqcoprm  26013  addsq2nreurex  26022  ostth2lem2  26212  ostth3  26216  ubthlem2  28650  nmopleid  29918  fsuppcurry1  30463  fsuppcurry2  30464  prmdvdsbc  30534  numdenneg  30535  pfxlsw2ccat  30628  wrdt2ind  30629  cyc3conja  30801  archirngz  30820  archiabllem1a  30822  fedgmullem1  31027  fedgmullem2  31028  submatminr1  31077  locfinreflem  31106  sxbrsigalem2  31546  oddpwdc  31614  ballotlemsdom  31771  ballotlemsel1i  31772  ballotlemsima  31775  ballotlemfrcn0  31789  fsum2dsub  31880  circlemeth  31913  elmrsubrn  32769  ismblfin  34935  itg2gt0cn  34949  cntotbnd  35076  ismtyhmeolem  35084  heibor1lem  35089  heiborlem6  35096  rrnequiv  35115  1cvrat  36614  ps-2b  36620  2at0mat0  36663  ps-2c  36666  llncvrlpln2  36695  2llnmeqat  36709  4atlem10  36744  4atlem11a  36745  4atlem12a  36748  2lplnja  36757  dalemcea  36798  dalem2  36799  dalem21  36832  dalem54  36864  2lnat  36922  cdlemb  36932  elpaddat  36942  paddasslem7  36964  paddasslem9  36966  paddasslem10  36967  paddasslem15  36972  poml6N  37093  osumcllem6N  37099  osumcllem7N  37100  pexmidlem4N  37111  pl42lem4N  37120  lhplt  37138  lhpjat1  37158  cdlemc5  37333  cdlemeg46fgN  37672  cdlemg12g  37787  tendoco2  37906  tendococl  37910  tendodi1  37922  tendoicl  37934  cdlemi2  37957  tendospdi1  38158  dihord11c  38362  dihmeetlem6  38447  dihjatc1  38449  dihmeetlem10N  38454  prodsplit  39103  expgcd  39190  fltnltalem  39281  jm2.20nn  39601  jm2.25  39603  kercvrlsm  39690  frege96d  40101  frege98d  40105  ntrclsk3  40427  binomcxplemnn0  40688  snunioo1  41795  limcleqr  41932  dvdivbd  42215  volioc  42264  iblspltprt  42265  volico  42275  stoweidlem1  42293  stoweidlem20  42312  stoweidlem24  42316  etransclem23  42549  iccpartipre  43588  2pwp1prm  43758  perfectALTVlem2  43894  lincresunit2  44540  expnegico01  44580  itscnhlinecirc02plem3  44778