Theorem 3pm3.2i 1358

Description: Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)

Hypotheses

Ref	Expression
3pm3.2i.1	⊢ 𝜑
3pm3.2i.2	⊢ 𝜓
3pm3.2i.3	⊢ 𝜒

Assertion

Ref	Expression
3pm3.2i	⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Proof of Theorem 3pm3.2i

Step	Hyp	Ref	Expression
1		3pm3.2i.1	. . 3 ⊢ 𝜑
2		3pm3.2i.2	. . 3 ⊢ 𝜓
3	1, 2	pm3.2i 476	. 2 ⊢ (𝜑 ∧ 𝜓)
4		3pm3.2i.3	. 2 ⊢ 𝜒
5		df-3an 1105	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
6	3, 4, 5	mpbir2an 724	1 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

This proof depends on syntax axioms:   ∧ 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:  mpbir3an  1360  3jaoiOLD  1455  ftp  7161  on2recsov  8663  hartogslem1  9514  cantnflem3  9670  cantnflem4  9671  trcl  9707  ttukeylem7  10517  f13idfv  14056  faclbnd4lem1  14349  4bc2eq6  14385  hashge3el3dif  14544  hash3tpb  14552  funcnvs3  14977  wrdl3s3  15025  infcvgaux1i  15937  halfleoddlt  16445  strleun  17242  strle1  17243  slotstnscsi  17438  slotsdnscsi  17470  slotsdifunifndx  17479  slotsbhcdif  17493  setc2obas  18176  estrres  18220  srgbinomlem4  20342  cnfldfunALT  21574  xrsnsgrp  21595  psrass1  22150  psrass23l  22153  psrass23  22155  mplsubrg  22191  mplmon  22223  mplmonmul  22224  mplcoe1  22225  mplbas2  22230  evlslem2  22267  coe1mul2  22467  zfbas  24090  ust0  24414  utop2nei  24444  isclmi0  25294  iscvsi  25325  plypf1  26406  1cubr  27044  birthdaylem1  27153  divsqrtsumlem  27181  lgslem2  27499  lgsdir2lem2  27527  lgsdir2lem3  27528  addsqn2reu  27642  addsqrexnreu  27643  addsqnreup  27644  nolt02o  27896  nogt01o  27897  noinds  28175  norecov  28177  norec2ov  28187  bdayfinbndlem1  28697  axlowdimlem6  29334  usgrexmpldifpr  29645  0grsubgr  29665  upgrewlkle2  29993  usgr2wlkspthlem2  30144  usgr2pthlem  30149  elwspths2spth  30356  wlk2v2e  30545  ntrl2v2e  30546  konigsberglem4  30643  konigsberglem5  30644  ex-dvds  30844  sspid  31114  lnocoi  31146  nmlno0lem  31182  nmblolbii  31188  blocnilem  31193  phpar  31213  ip0i  31214  ip2i  31217  ipdirilem  31218  ipasslem10  31228  ip2dii  31233  siilem1  31240  siilem2  31241  hhssabloilem  31650  hhsst  31655  hhsssh2  31659  fh1i  32010  fh2i  32011  cm2ji  32014  pjoi0i  32107  elunop2  32402  mdslle1i  32706  mdslle2i  32707  mdslj1i  32708  mdslj2i  32709  mdslmd1lem1  32714  mdslmd2i  32719  dp2lt  33241  dpadd3  33268  threehalves  33271  cyc3evpm  33501  xrge0slmod  33699  zringfrac  33875  psrmonmul  33971  cos9thpiminplylem5  34207  xrge0iifmhm  34360  cnzh  34389  rezh  34390  dmvlsiga  34550  eulerpartgbij  34794  hgt750lemd  35067  hgt750lem  35070  hgt750lemb  35075  hgt750leme  35077  tz9.1regs  35571  dnizeq0  37105  cnndvlem1  37167  taupi  38008  poimirlem28  38340  poimirlem31  38343  poimirlem32  38344  asindmre  38395  areacirc  38405  ishlatiN  40170  gcdaddmzz2nni  42802  lcmeprodgcdi  42815  3lexlogpow5ineq1  42862  3lexlogpow2ineq1  42866  rabren3dioph  43583  oaomoencom  44085  inductionexd  44922  lhe4.4ex1a  45080  stoweidlem13  46768  stoweidlem26  46781  stoweidlem34  46789  stoweid  46818  wallispilem2  46821  fourierdlem62  46923  fourierdlem103  46964  fouriersw  46986  salexct3  47097  salgensscntex  47099  smfmullem4  47549  pldofph  47723  31prm  48390  9fppr8  48543  6gbe  48577  8gbe  48579  9gbo  48580  11gbo  48581  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  nnsum4primeseven  48606  tgblthelfgott  48621  tgoldbach  48623  usgrexmpl1lem  48827  usgrexmpl1tri  48831  usgrexmpl2lem  48832  gpg5grlim  48899  gpg5grlic  48900  gpgprismgr4cycllem2  48902  zlmodzxzldeplem3  49323  zlmodzxzldep  49325  blennnt2  49410  fv2arycl  49469  2arymptfv  49471  line2  49573  line2x  49575  line2y  49576  setc1onsubc  50421  2elfz13  50667  crosspdotsumi  50687