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  7152  on2recsov  8664  hartogslem1  9534  cantnflem3  9683  cantnflem4  9684  trcl  9720  ttukeylem7  10507  f13idfv  13962  faclbnd4lem1  14250  4bc2eq6  14286  hashge3el3dif  14444  funcnvs3  14862  wrdl3s3  14910  infcvgaux1i  15800  halfleoddlt  16302  strleun  17087  strle1  17088  slotstnscsi  17302  slotsdnscsi  17334  slotsdifunifndx  17343  slotsbhcdif  17357  slotsbhcdifOLD  17358  setc2obas  18041  estrres  18088  srgbinomlem4  20046  cnfldfunALT  20950  cnfldfunALTOLD  20951  xrsnsgrp  20974  psrass1  21517  psrass23l  21520  psrass23  21522  mplsubrg  21556  mplmon  21582  mplmonmul  21583  mplcoe1  21584  mplbas2  21589  evlslem2  21634  coe1mul2  21783  zfbas  23392  ust0  23716  utop2nei  23747  isclmi0  24606  iscvsi  24637  plypf1  25718  1cubr  26337  birthdaylem1  26446  divsqrtsumlem  26474  lgslem2  26791  lgsdir2lem2  26819  lgsdir2lem3  26820  addsqn2reu  26934  addsqrexnreu  26935  addsqnreup  26936  nolt02o  27188  nogt01o  27189  noinds  27419  norecov  27421  norec2ov  27431  axlowdimlem6  28195  usgrexmpldifpr  28505  0grsubgr  28525  upgrewlkle2  28853  usgr2wlkspthlem2  29005  usgr2pthlem  29010  elwspths2spth  29211  wlk2v2e  29400  ntrl2v2e  29401  konigsberglem4  29498  konigsberglem5  29499  ex-dvds  29699  sspid  29966  lnocoi  29998  nmlno0lem  30034  nmblolbii  30040  blocnilem  30045  phpar  30065  ip0i  30066  ip2i  30069  ipdirilem  30070  ipasslem10  30080  ip2dii  30085  siilem1  30092  siilem2  30093  hhssabloilem  30502  hhsst  30507  hhsssh2  30511  fh1i  30862  fh2i  30863  cm2ji  30866  pjoi0i  30959  elunop2  31254  mdslle1i  31558  mdslle2i  31559  mdslj1i  31560  mdslj2i  31561  mdslmd1lem1  31566  mdslmd2i  31571  dp2lt  32039  dpadd3  32066  threehalves  32069  cyc3evpm  32297  xrge0slmod  32452  xrge0iifmhm  32908  cnzh  32939  rezh  32940  dmvlsiga  33116  eulerpartgbij  33360  hgt750lemd  33649  hgt750lem  33652  hgt750lemb  33657  hgt750leme  33659  dnizeq0  35340  cnndvlem1  35402  taupi  36193  poimirlem28  36505  poimirlem31  36508  poimirlem32  36509  asindmre  36560  areacirc  36570  ishlatiN  38214  gcdaddmzz2nni  40849  lcmeprodgcdi  40861  3lexlogpow5ineq1  40908  3lexlogpow2ineq1  40912  rabren3dioph  41539  oaomoencom  42053  inductionexd  42892  lhe4.4ex1a  43074  stoweidlem13  44716  stoweidlem26  44729  stoweidlem34  44737  stoweid  44766  wallispilem2  44769  fourierdlem62  44871  fourierdlem103  44912  fouriersw  44934  salexct3  45045  salgensscntex  45047  smfmullem4  45497  pldofph  45642  31prm  46252  9fppr8  46392  6gbe  46426  8gbe  46428  9gbo  46429  11gbo  46430  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  nnsum4primeseven  46455  tgblthelfgott  46470  tgoldbach  46472  zlmodzxzldeplem3  47137  zlmodzxzldep  47139  blennnt2  47229  fv2arycl  47288  2arymptfv  47290  line2  47392  line2x  47394  line2y  47395