Theorem syl32anc 1376

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  coftr  10270  fin1a2s  10411  ioounsn  13458  snunioo  13459  snunico  13460  snunioc  13461  exple1  14145  leexp2rd  14222  facubnd  14264  permnn  14290  sqgcd  16506  cncongr2  16609  hashgcdlem  16725  ramlb  16956  0ram  16957  ram0  16959  ramz2  16961  ramz  16962  ramcl  16966  lsmub1x  19555  lsmub2x  19556  lsmsubm  19562  pgpfac1lem2  19986  mptscmfsupp0  20681  2idlcpblrng  21020  xrsdsreclblem  21191  pzriprnglem12  21261  uvcff  21565  uvcresum  21567  frlmup1  21572  psrass1lemOLD  21712  psrass1lem  21715  psrlidm  21742  psrridm  21743  psrcom  21748  mvrcl  21770  mplsubrglem  21782  mplcoe5  21814  mplbas2  21816  psrbagev1  21857  psrbagev1OLD  21858  evlslem3  21862  evlslem6  21863  psropprmul  21980  smadiadetg  22395  cayhamlem4  22610  lecldbas  22943  pnfnei  22944  mnfnei  22945  clsconn  23154  txcls  23328  ufldom  23686  hauspwpwf1  23711  flfcnp  23728  flfcnp2  23731  cnpfcfi  23764  tsmsmhm  23870  met2ndci  24251  nghmco  24475  nghmplusg  24477  icopnfcld  24504  iocmnfcld  24505  tgioo  24532  reconnlem1  24562  metdseq0  24590  ovolunnul  25249  volinun  25295  volfiniun  25296  volsup  25305  icombl  25313  ioombl  25314  ovolioo  25317  ioorcl2  25321  volivth  25356  ismbf3d  25403  dvferm2lem  25738  lhop  25768  tayl0  26110  pserulm  26170  cxpcn3  26492  ssscongptld  26563  heron  26579  dvdsmulf1o  26934  logexprlim  26964  perfectlem2  26969  lgssq  27076  lgssq2  27077  gausslemma2dlem7  27112  lgsquad2lem1  27123  lgsquad2lem2  27124  2sqblem  27170  addsq2nreurex  27183  ostth2lem2  27373  ostth3  27377  ubthlem2  30391  nmopleid  31659  fsuppcurry1  32217  fsuppcurry2  32218  prmdvdsbc  32289  numdenneg  32290  mgcf1olem1  32438  mgcf1olem2  32439  gsummptres2  32475  archirngz  32605  archiabllem1a  32607  evls1fpws  32920  q1pdir  32948  q1pvsca  32949  ply1degltdimlem  32995  fedgmullem1  33002  fedgmullem2  33003  evls1fldgencl  33033  submatminr1  33088  locfinreflem  33118  sxbrsigalem2  33583  elmrsubrn  34809  ismblfin  36832  itg2gt0cn  36846  cntotbnd  36967  ismtyhmeolem  36975  heibor1lem  36980  heiborlem6  36987  rrnequiv  37006  1cvrat  38650  ps-2b  38656  2at0mat0  38699  ps-2c  38702  llncvrlpln2  38731  2llnmeqat  38745  4atlem10  38780  4atlem11a  38781  4atlem12a  38784  2lplnja  38793  dalemcea  38834  dalem2  38835  dalem21  38868  dalem54  38900  2lnat  38958  cdlemb  38968  elpaddat  38978  paddasslem7  39000  paddasslem9  39002  paddasslem10  39003  paddasslem15  39008  poml6N  39129  osumcllem6N  39135  osumcllem7N  39136  pexmidlem4N  39147  pl42lem4N  39156  lhplt  39174  lhpjat1  39194  cdlemc5  39369  cdlemeg46fgN  39708  cdlemg12g  39823  tendoco2  39942  tendococl  39946  tendodi1  39958  tendoicl  39970  cdlemi2  39993  tendospdi1  40194  dihord11c  40398  dihmeetlem6  40483  dihjatc1  40485  dihmeetlem10N  40490  fsuppsssuppgd  41370  expgcd  41527  fltnltalem  41706  jm2.20nn  42038  kercvrlsm  42127  omord2lim  42352  frege96d  42802  frege98d  42806  ntrclsk3  43123  snunioo1  44523  limcleqr  44658  dvdivbd  44937  volioc  44986  iblspltprt  44987  volico  44997  stoweidlem1  45015  stoweidlem24  45038  etransclem23  45271  iccpartipre  46387  2pwp1prm  46555  perfectALTVlem2  46688  lincresunit2  47246  expnegico01  47286  itscnhlinecirc02plem3  47557