Theorem 3pm3.2i 1356

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

Syntax hints:   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  mpbir3an  1358  3jaoiOLD  1451  ftp  7144  on2recsov  8642  hartogslem1  9492  cantnflem3  9648  cantnflem4  9649  trcl  9685  ttukeylem7  10487  f13idfv  14027  faclbnd4lem1  14320  4bc2eq6  14356  hashge3el3dif  14514  hash3tpb  14522  funcnvs3  14941  wrdl3s3  14989  infcvgaux1i  15901  halfleoddlt  16410  strleun  17207  strle1  17208  slotstnscsi  17403  slotsdnscsi  17435  slotsdifunifndx  17444  slotsbhcdif  17458  setc2obas  18141  estrres  18185  srgbinomlem4  20302  cnfldfunALT  21497  xrsnsgrp  21518  psrass1  22073  psrass23l  22076  psrass23  22078  mplsubrg  22114  mplmon  22146  mplmonmul  22147  mplcoe1  22148  mplbas2  22153  evlslem2  22190  coe1mul2  22390  zfbas  24014  ust0  24338  utop2nei  24368  isclmi0  25218  iscvsi  25249  plypf1  26330  1cubr  26965  birthdaylem1  27074  divsqrtsumlem  27102  lgslem2  27420  lgsdir2lem2  27448  lgsdir2lem3  27449  addsqn2reu  27563  addsqrexnreu  27564  addsqnreup  27565  nolt02o  27817  nogt01o  27818  noinds  28096  norecov  28098  norec2ov  28108  bdayfinbndlem1  28618  axlowdimlem6  29206  usgrexmpldifpr  29517  0grsubgr  29537  upgrewlkle2  29865  usgr2wlkspthlem2  30016  usgr2pthlem  30021  elwspths2spth  30228  wlk2v2e  30417  ntrl2v2e  30418  konigsberglem4  30515  konigsberglem5  30516  ex-dvds  30716  sspid  30986  lnocoi  31018  nmlno0lem  31054  nmblolbii  31060  blocnilem  31065  phpar  31085  ip0i  31086  ip2i  31089  ipdirilem  31090  ipasslem10  31100  ip2dii  31105  siilem1  31112  siilem2  31113  hhssabloilem  31522  hhsst  31527  hhsssh2  31531  fh1i  31882  fh2i  31883  cm2ji  31886  pjoi0i  31979  elunop2  32274  mdslle1i  32578  mdslle2i  32579  mdslj1i  32580  mdslj2i  32581  mdslmd1lem1  32586  mdslmd2i  32591  dp2lt  33117  dpadd3  33144  threehalves  33147  cyc3evpm  33383  xrge0slmod  33583  zringfrac  33761  psrmonmul  33857  cos9thpiminplylem5  34093  xrge0iifmhm  34246  cnzh  34275  rezh  34276  dmvlsiga  34436  eulerpartgbij  34679  hgt750lemd  34952  hgt750lem  34955  hgt750lemb  34960  hgt750leme  34962  tz9.1regs  35442  dnizeq0  36926  cnndvlem1  36988  taupi  37827  poimirlem28  38159  poimirlem31  38162  poimirlem32  38163  asindmre  38214  areacirc  38224  ishlatiN  39991  gcdaddmzz2nni  42623  lcmeprodgcdi  42636  3lexlogpow5ineq1  42683  3lexlogpow2ineq1  42687  rabren3dioph  43404  oaomoencom  43906  inductionexd  44743  lhe4.4ex1a  44903  stoweidlem13  46585  stoweidlem26  46598  stoweidlem34  46606  stoweid  46635  wallispilem2  46638  fourierdlem62  46740  fourierdlem103  46781  fouriersw  46803  salexct3  46914  salgensscntex  46916  smfmullem4  47366  pldofph  47537  31prm  48204  9fppr8  48357  6gbe  48391  8gbe  48393  9gbo  48394  11gbo  48395  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  nnsum4primeseven  48420  tgblthelfgott  48435  tgoldbach  48437  usgrexmpl1lem  48641  usgrexmpl1tri  48645  usgrexmpl2lem  48646  gpg5grlim  48713  gpg5grlic  48714  gpgprismgr4cycllem2  48716  zlmodzxzldeplem3  49133  zlmodzxzldep  49135  blennnt2  49220  fv2arycl  49279  2arymptfv  49281  line2  49383  line2x  49385  line2y  49386  setc1onsubc  50231