Theorem 3pm3.2i 1341

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 712	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  1343  3jaoi  1431  ftp  7111  on2recsov  8604  hartogslem1  9457  cantnflem3  9612  cantnflem4  9613  trcl  9649  ttukeylem7  10437  f13idfv  13962  faclbnd4lem1  14255  4bc2eq6  14291  hashge3el3dif  14449  hash3tpb  14457  funcnvs3  14876  wrdl3s3  14924  infcvgaux1i  15822  halfleoddlt  16331  strleun  17127  strle1  17128  slotstnscsi  17323  slotsdnscsi  17355  slotsdifunifndx  17364  slotsbhcdif  17378  setc2obas  18061  estrres  18105  srgbinomlem4  20210  cnfldfunALT  21367  xrsnsgrp  21388  psrass1  21942  psrass23l  21945  psrass23  21947  mplsubrg  21983  mplmon  22013  mplmonmul  22014  mplcoe1  22015  mplbas2  22020  evlslem2  22057  coe1mul2  22234  zfbas  23861  ust0  24185  utop2nei  24215  isclmi0  25065  iscvsi  25096  plypf1  26177  1cubr  26806  birthdaylem1  26915  divsqrtsumlem  26943  lgslem2  27261  lgsdir2lem2  27289  lgsdir2lem3  27290  addsqn2reu  27404  addsqrexnreu  27405  addsqnreup  27406  nolt02o  27659  nogt01o  27660  noinds  27937  norecov  27939  norec2ov  27949  bdayfinbndlem1  28459  axlowdimlem6  29016  usgrexmpldifpr  29327  0grsubgr  29347  upgrewlkle2  29675  usgr2wlkspthlem2  29826  usgr2pthlem  29831  elwspths2spth  30038  wlk2v2e  30227  ntrl2v2e  30228  konigsberglem4  30325  konigsberglem5  30326  ex-dvds  30526  sspid  30796  lnocoi  30828  nmlno0lem  30864  nmblolbii  30870  blocnilem  30875  phpar  30895  ip0i  30896  ip2i  30899  ipdirilem  30900  ipasslem10  30910  ip2dii  30915  siilem1  30922  siilem2  30923  hhssabloilem  31332  hhsst  31337  hhsssh2  31341  fh1i  31692  fh2i  31693  cm2ji  31696  pjoi0i  31789  elunop2  32084  mdslle1i  32388  mdslle2i  32389  mdslj1i  32390  mdslj2i  32391  mdslmd1lem1  32396  mdslmd2i  32401  dp2lt  32944  dpadd3  32971  threehalves  32974  cyc3evpm  33211  xrge0slmod  33408  zringfrac  33614  psrmonmul  33694  cos9thpiminplylem5  33930  xrge0iifmhm  34083  cnzh  34112  rezh  34113  dmvlsiga  34273  eulerpartgbij  34516  hgt750lemd  34792  hgt750lem  34795  hgt750lemb  34800  hgt750leme  34802  tz9.1regs  35278  dnizeq0  36735  cnndvlem1  36797  taupi  37637  poimirlem28  37969  poimirlem31  37972  poimirlem32  37973  asindmre  38024  areacirc  38034  ishlatiN  39801  gcdaddmzz2nni  42433  lcmeprodgcdi  42446  3lexlogpow5ineq1  42493  3lexlogpow2ineq1  42497  rabren3dioph  43243  oaomoencom  43745  inductionexd  44582  lhe4.4ex1a  44756  stoweidlem13  46441  stoweidlem26  46454  stoweidlem34  46462  stoweid  46491  wallispilem2  46494  fourierdlem62  46596  fourierdlem103  46637  fouriersw  46659  salexct3  46770  salgensscntex  46772  smfmullem4  47222  pldofph  47393  31prm  48060  9fppr8  48213  6gbe  48247  8gbe  48249  9gbo  48250  11gbo  48251  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  tgblthelfgott  48291  tgoldbach  48293  usgrexmpl1lem  48497  usgrexmpl1tri  48501  usgrexmpl2lem  48502  gpg5grlim  48569  gpg5grlic  48570  gpgprismgr4cycllem2  48572  zlmodzxzldeplem3  48978  zlmodzxzldep  48980  blennnt2  49065  fv2arycl  49124  2arymptfv  49126  line2  49228  line2x  49230  line2y  49231  setc1onsubc  50077