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  8680  hartogslem1  9539  cantnflem3  9695  cantnflem4  9696  trcl  9732  ttukeylem7  10596  f13idfv  14146  faclbnd4lem1  14440  4bc2eq6  14476  hashge3el3dif  14635  hash3tpb  14643  funcnvs3  15070  wrdl3s3  15120  infcvgaux1i  16031  halfleoddlt  16537  strleun  17340  strle1  17341  slotstnscsi  17536  slotsdnscsi  17568  slotsdifunifndx  17577  slotsbhcdif  17591  setc2obas  18274  estrres  18318  srgbinomlem4  20460  cnfldfunALT  21698  xrsnsgrp  21719  psrass1  22276  psrass23l  22279  psrass23  22281  mplsubrg  22317  mplmon  22349  mplmonmul  22350  mplcoe1  22351  mplbas2  22356  evlslem2  22393  coe1mul2  22593  zfbas  24220  ust0  24544  utop2nei  24574  isclmi0  25424  iscvsi  25455  plypf1  26536  1cubr  27175  birthdaylem1  27284  divsqrtsumlem  27312  lgslem2  27630  lgsdir2lem2  27658  lgsdir2lem3  27659  addsqn2reu  27773  addsqrexnreu  27774  addsqnreup  27775  nolt02o  28057  nogt01o  28058  noinds  28336  norecov  28338  norec2ov  28348  bdayfinbndlem1  28858  axlowdimlem6  29530  usgrexmpldifpr  29844  0grsubgr  29864  upgrewlkle2  30192  usgr2wlkspthlem2  30349  usgr2pthlem  30354  elwspths2spth  30564  wlk2v2e  30763  ntrl2v2e  30764  konigsberglem4  30861  konigsberglem5  30862  ex-dvds  31062  sspid  31332  lnocoi  31364  nmlno0lem  31400  nmblolbii  31406  blocnilem  31411  phpar  31431  ip0i  31432  ip2i  31435  ipdirilem  31436  ipasslem10  31446  ip2dii  31451  siilem1  31458  siilem2  31459  hhssabloilem  31868  hhsst  31873  hhsssh2  31877  fh1i  32228  fh2i  32229  cm2ji  32232  pjoi0i  32325  elunop2  32620  mdslle1i  32924  mdslle2i  32925  mdslj1i  32926  mdslj2i  32927  mdslmd1lem1  32932  mdslmd2i  32937  dp2lt  33497  dpadd3  33524  threehalves  33527  cyc3evpm  33757  xrge0slmod  33955  zringfrac  34132  psrmonmul  34228  cos9thpiminplylem5  34464  xrge0iifmhm  34617  cnzh  34646  rezh  34647  dmvlsiga  34807  eulerpartgbij  35050  hgt750lemd  35323  hgt750lem  35326  hgt750lemb  35331  hgt750leme  35333  tz9.1regs  35858  dnizeq0  37433  cnndvlem1  37495  taupi  38337  poimirlem28  38659  poimirlem31  38662  poimirlem32  38663  asindmre  38714  areacirc  38724  ishlatiN  40505  gcdaddmzz2nni  43137  lcmeprodgcdi  43150  3lexlogpow5ineq1  43197  3lexlogpow2ineq1  43201  rabren3dioph  43915  oaomoencom  44412  inductionexd  45248  lhe4.4ex1a  45406  stoweidlem13  47116  stoweidlem26  47129  stoweidlem34  47137  stoweid  47166  wallispilem2  47169  fourierdlem62  47271  fourierdlem103  47312  fouriersw  47334  salexct3  47445  salgensscntex  47447  smfmullem4  47897  pldofph  48108  31prm  48775  9fppr8  48928  6gbe  48962  8gbe  48964  9gbo  48965  11gbo  48966  nnsum4primesodd  48987  nnsum4primesoddALTV  48988  nnsum4primeseven  48991  tgblthelfgott  49006  tgoldbach  49008  usgrexmpl1lem  49212  usgrexmpl1tri  49216  usgrexmpl2lem  49217  gpg5grlim  49284  gpg5grlic  49285  gpgprismgr4cycllem2  49287  zlmodzxzldeplem3  49707  zlmodzxzldep  49709  blennnt2  49794  fv2arycl  49853  2arymptfv  49855  setc1onsubc  50833  par2str  50862  parswapprop  50870  par2hom  50872  crosspdotsumlem  51132