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

Syntax hints:   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  mpbir3an  1342  3jaoi  1428  ftp  7142  on2recsov  8655  hartogslem1  9524  cantnflem3  9673  cantnflem4  9674  trcl  9710  ttukeylem7  10497  f13idfv  13952  faclbnd4lem1  14240  4bc2eq6  14276  hashge3el3dif  14434  funcnvs3  14852  wrdl3s3  14900  infcvgaux1i  15790  halfleoddlt  16292  strleun  17077  strle1  17078  slotstnscsi  17292  slotsdnscsi  17324  slotsdifunifndx  17333  slotsbhcdif  17347  slotsbhcdifOLD  17348  setc2obas  18031  estrres  18078  srgbinomlem4  20034  cnfldfunALT  20931  cnfldfunALTOLD  20932  xrsnsgrp  20955  psrass1  21496  psrass23l  21499  psrass23  21501  mplsubrg  21533  mplmon  21558  mplmonmul  21559  mplcoe1  21560  mplbas2  21565  evlslem2  21611  coe1mul2  21762  zfbas  23369  ust0  23693  utop2nei  23724  isclmi0  24583  iscvsi  24614  plypf1  25695  1cubr  26314  birthdaylem1  26423  divsqrtsumlem  26451  lgslem2  26768  lgsdir2lem2  26796  lgsdir2lem3  26797  addsqn2reu  26911  addsqrexnreu  26912  addsqnreup  26913  nolt02o  27165  nogt01o  27166  noinds  27396  norecov  27398  norec2ov  27408  axlowdimlem6  28172  usgrexmpldifpr  28482  0grsubgr  28502  upgrewlkle2  28830  usgr2wlkspthlem2  28982  usgr2pthlem  28987  elwspths2spth  29188  wlk2v2e  29377  ntrl2v2e  29378  konigsberglem4  29475  konigsberglem5  29476  ex-dvds  29676  sspid  29943  lnocoi  29975  nmlno0lem  30011  nmblolbii  30017  blocnilem  30022  phpar  30042  ip0i  30043  ip2i  30046  ipdirilem  30047  ipasslem10  30057  ip2dii  30062  siilem1  30069  siilem2  30070  hhssabloilem  30479  hhsst  30484  hhsssh2  30488  fh1i  30839  fh2i  30840  cm2ji  30843  pjoi0i  30936  elunop2  31231  mdslle1i  31535  mdslle2i  31536  mdslj1i  31537  mdslj2i  31538  mdslmd1lem1  31543  mdslmd2i  31548  dp2lt  32022  dpadd3  32049  threehalves  32052  cyc3evpm  32280  xrge0slmod  32425  xrge0iifmhm  32850  cnzh  32881  rezh  32882  dmvlsiga  33058  eulerpartgbij  33302  hgt750lemd  33591  hgt750lem  33594  hgt750lemb  33599  hgt750leme  33601  dnizeq0  35256  cnndvlem1  35318  taupi  36109  poimirlem28  36421  poimirlem31  36424  poimirlem32  36425  asindmre  36476  areacirc  36486  ishlatiN  38131  gcdaddmzz2nni  40766  lcmeprodgcdi  40778  3lexlogpow5ineq1  40825  3lexlogpow2ineq1  40829  rabren3dioph  41424  oaomoencom  41938  inductionexd  42777  lhe4.4ex1a  42959  stoweidlem13  44602  stoweidlem26  44615  stoweidlem34  44623  stoweid  44652  wallispilem2  44655  fourierdlem62  44757  fourierdlem103  44798  fouriersw  44820  salexct3  44931  salgensscntex  44933  smfmullem4  45383  pldofph  45528  31prm  46138  9fppr8  46278  6gbe  46312  8gbe  46314  9gbo  46315  11gbo  46316  nnsum4primesodd  46337  nnsum4primesoddALTV  46338  nnsum4primeseven  46341  tgblthelfgott  46356  tgoldbach  46358  zlmodzxzldeplem3  47023  zlmodzxzldep  47025  blennnt2  47115  fv2arycl  47174  2arymptfv  47176  line2  47278  line2x  47280  line2y  47281