Theorem 3pm3.2i 1339

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 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
6	3, 4, 5	mpbir2an 710	1 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Syntax hints:   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  mpbir3an  1341  3jaoi  1428  ftp  7191  on2recsov  8724  hartogslem1  9611  cantnflem3  9760  cantnflem4  9761  trcl  9797  ttukeylem7  10584  f13idfv  14051  faclbnd4lem1  14342  4bc2eq6  14378  hashge3el3dif  14536  hash3tpb  14544  funcnvs3  14963  wrdl3s3  15011  infcvgaux1i  15905  halfleoddlt  16410  strleun  17204  strle1  17205  slotstnscsi  17419  slotsdnscsi  17451  slotsdifunifndx  17460  slotsbhcdif  17474  slotsbhcdifOLD  17475  setc2obas  18161  estrres  18208  srgbinomlem4  20256  cnfldfunALT  21402  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  xrsnsgrp  21443  psrass1  22007  psrass23l  22010  psrass23  22012  mplsubrg  22048  mplmon  22076  mplmonmul  22077  mplcoe1  22078  mplbas2  22083  evlslem2  22126  coe1mul2  22293  zfbas  23925  ust0  24249  utop2nei  24280  isclmi0  25150  iscvsi  25181  plypf1  26271  1cubr  26903  birthdaylem1  27012  divsqrtsumlem  27041  lgslem2  27360  lgsdir2lem2  27388  lgsdir2lem3  27389  addsqn2reu  27503  addsqrexnreu  27504  addsqnreup  27505  nolt02o  27758  nogt01o  27759  noinds  27996  norecov  27998  norec2ov  28008  nohalf  28425  axlowdimlem6  28980  usgrexmpldifpr  29293  0grsubgr  29313  upgrewlkle2  29642  usgr2wlkspthlem2  29794  usgr2pthlem  29799  elwspths2spth  30000  wlk2v2e  30189  ntrl2v2e  30190  konigsberglem4  30287  konigsberglem5  30288  ex-dvds  30488  sspid  30757  lnocoi  30789  nmlno0lem  30825  nmblolbii  30831  blocnilem  30836  phpar  30856  ip0i  30857  ip2i  30860  ipdirilem  30861  ipasslem10  30871  ip2dii  30876  siilem1  30883  siilem2  30884  hhssabloilem  31293  hhsst  31298  hhsssh2  31302  fh1i  31653  fh2i  31654  cm2ji  31657  pjoi0i  31750  elunop2  32045  mdslle1i  32349  mdslle2i  32350  mdslj1i  32351  mdslj2i  32352  mdslmd1lem1  32357  mdslmd2i  32362  dp2lt  32849  dpadd3  32876  threehalves  32879  cyc3evpm  33143  xrge0slmod  33341  zringfrac  33547  xrge0iifmhm  33885  cnzh  33916  rezh  33917  dmvlsiga  34093  eulerpartgbij  34337  hgt750lemd  34625  hgt750lem  34628  hgt750lemb  34633  hgt750leme  34635  dnizeq0  36441  cnndvlem1  36503  taupi  37289  poimirlem28  37608  poimirlem31  37611  poimirlem32  37612  asindmre  37663  areacirc  37673  ishlatiN  39311  gcdaddmzz2nni  41951  lcmeprodgcdi  41964  3lexlogpow5ineq1  42011  3lexlogpow2ineq1  42015  rabren3dioph  42771  oaomoencom  43279  inductionexd  44117  lhe4.4ex1a  44298  stoweidlem13  45934  stoweidlem26  45947  stoweidlem34  45955  stoweid  45984  wallispilem2  45987  fourierdlem62  46089  fourierdlem103  46130  fouriersw  46152  salexct3  46263  salgensscntex  46265  smfmullem4  46715  pldofph  46860  31prm  47471  9fppr8  47611  6gbe  47645  8gbe  47647  9gbo  47648  11gbo  47649  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  tgblthelfgott  47689  tgoldbach  47691  usgrexmpl1lem  47836  usgrexmpl1tri  47840  usgrexmpl2lem  47841  zlmodzxzldeplem3  48231  zlmodzxzldep  48233  blennnt2  48323  fv2arycl  48382  2arymptfv  48384  line2  48486  line2x  48488  line2y  48489