Theorem 3pm3.2i 1340

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 470	. 2 ⊢ (𝜑 ∧ 𝜓)
4		3pm3.2i.3	. 2 ⊢ 𝜒
5		df-3an 1088	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
6	3, 4, 5	mpbir2an 711	1 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Syntax hints:   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  mpbir3an  1342  3jaoi  1430  ftp  7090  on2recsov  8583  hartogslem1  9428  cantnflem3  9581  cantnflem4  9582  trcl  9618  ttukeylem7  10403  f13idfv  13904  faclbnd4lem1  14197  4bc2eq6  14233  hashge3el3dif  14391  hash3tpb  14399  funcnvs3  14818  wrdl3s3  14866  infcvgaux1i  15761  halfleoddlt  16270  strleun  17065  strle1  17066  slotstnscsi  17261  slotsdnscsi  17293  slotsdifunifndx  17302  slotsbhcdif  17316  setc2obas  17998  estrres  18042  srgbinomlem4  20145  cnfldfunALT  21304  cnfldfunALTOLD  21317  xrsnsgrp  21342  psrass1  21899  psrass23l  21902  psrass23  21904  mplsubrg  21940  mplmon  21968  mplmonmul  21969  mplcoe1  21970  mplbas2  21975  evlslem2  22012  coe1mul2  22181  zfbas  23809  ust0  24133  utop2nei  24163  isclmi0  25023  iscvsi  25054  plypf1  26142  1cubr  26777  birthdaylem1  26886  divsqrtsumlem  26915  lgslem2  27234  lgsdir2lem2  27262  lgsdir2lem3  27263  addsqn2reu  27377  addsqrexnreu  27378  addsqnreup  27379  nolt02o  27632  nogt01o  27633  noinds  27886  norecov  27888  norec2ov  27898  axlowdimlem6  28923  usgrexmpldifpr  29234  0grsubgr  29254  upgrewlkle2  29583  usgr2wlkspthlem2  29734  usgr2pthlem  29739  elwspths2spth  29943  wlk2v2e  30132  ntrl2v2e  30133  konigsberglem4  30230  konigsberglem5  30231  ex-dvds  30431  sspid  30700  lnocoi  30732  nmlno0lem  30768  nmblolbii  30774  blocnilem  30779  phpar  30799  ip0i  30800  ip2i  30803  ipdirilem  30804  ipasslem10  30814  ip2dii  30819  siilem1  30826  siilem2  30827  hhssabloilem  31236  hhsst  31241  hhsssh2  31245  fh1i  31596  fh2i  31597  cm2ji  31600  pjoi0i  31693  elunop2  31988  mdslle1i  32292  mdslle2i  32293  mdslj1i  32294  mdslj2i  32295  mdslmd1lem1  32300  mdslmd2i  32305  dp2lt  32860  dpadd3  32887  threehalves  32890  cyc3evpm  33114  xrge0slmod  33308  zringfrac  33514  cos9thpiminplylem5  33794  xrge0iifmhm  33947  cnzh  33976  rezh  33977  dmvlsiga  34137  eulerpartgbij  34380  hgt750lemd  34656  hgt750lem  34659  hgt750lemb  34664  hgt750leme  34666  tz9.1regs  35118  dnizeq0  36508  cnndvlem1  36570  taupi  37356  poimirlem28  37687  poimirlem31  37690  poimirlem32  37691  asindmre  37742  areacirc  37752  ishlatiN  39393  gcdaddmzz2nni  42026  lcmeprodgcdi  42039  3lexlogpow5ineq1  42086  3lexlogpow2ineq1  42090  rabren3dioph  42847  oaomoencom  43349  inductionexd  44187  lhe4.4ex1a  44361  stoweidlem13  46050  stoweidlem26  46063  stoweidlem34  46071  stoweid  46100  wallispilem2  46103  fourierdlem62  46205  fourierdlem103  46246  fouriersw  46268  salexct3  46379  salgensscntex  46381  smfmullem4  46831  pldofph  46975  31prm  47627  9fppr8  47767  6gbe  47801  8gbe  47803  9gbo  47804  11gbo  47805  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  nnsum4primeseven  47830  tgblthelfgott  47845  tgoldbach  47847  usgrexmpl1lem  48051  usgrexmpl1tri  48055  usgrexmpl2lem  48056  gpg5grlim  48123  gpg5grlic  48124  gpgprismgr4cycllem2  48126  zlmodzxzldeplem3  48533  zlmodzxzldep  48535  blennnt2  48620  fv2arycl  48679  2arymptfv  48681  line2  48783  line2x  48785  line2y  48786  setc1onsubc  49633