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  7155  on2recsov  8667  hartogslem1  9537  cantnflem3  9686  cantnflem4  9687  trcl  9723  ttukeylem7  10510  f13idfv  13965  faclbnd4lem1  14253  4bc2eq6  14289  hashge3el3dif  14447  funcnvs3  14865  wrdl3s3  14913  infcvgaux1i  15803  halfleoddlt  16305  strleun  17090  strle1  17091  slotstnscsi  17305  slotsdnscsi  17337  slotsdifunifndx  17346  slotsbhcdif  17360  slotsbhcdifOLD  17361  setc2obas  18044  estrres  18091  srgbinomlem4  20052  cnfldfunALT  20957  cnfldfunALTOLD  20958  xrsnsgrp  20981  psrass1  21525  psrass23l  21528  psrass23  21530  mplsubrg  21564  mplmon  21590  mplmonmul  21591  mplcoe1  21592  mplbas2  21597  evlslem2  21642  coe1mul2  21791  zfbas  23400  ust0  23724  utop2nei  23755  isclmi0  24614  iscvsi  24645  plypf1  25726  1cubr  26347  birthdaylem1  26456  divsqrtsumlem  26484  lgslem2  26801  lgsdir2lem2  26829  lgsdir2lem3  26830  addsqn2reu  26944  addsqrexnreu  26945  addsqnreup  26946  nolt02o  27198  nogt01o  27199  noinds  27429  norecov  27431  norec2ov  27441  axlowdimlem6  28205  usgrexmpldifpr  28515  0grsubgr  28535  upgrewlkle2  28863  usgr2wlkspthlem2  29015  usgr2pthlem  29020  elwspths2spth  29221  wlk2v2e  29410  ntrl2v2e  29411  konigsberglem4  29508  konigsberglem5  29509  ex-dvds  29709  sspid  29978  lnocoi  30010  nmlno0lem  30046  nmblolbii  30052  blocnilem  30057  phpar  30077  ip0i  30078  ip2i  30081  ipdirilem  30082  ipasslem10  30092  ip2dii  30097  siilem1  30104  siilem2  30105  hhssabloilem  30514  hhsst  30519  hhsssh2  30523  fh1i  30874  fh2i  30875  cm2ji  30878  pjoi0i  30971  elunop2  31266  mdslle1i  31570  mdslle2i  31571  mdslj1i  31572  mdslj2i  31573  mdslmd1lem1  31578  mdslmd2i  31583  dp2lt  32051  dpadd3  32078  threehalves  32081  cyc3evpm  32309  xrge0slmod  32463  xrge0iifmhm  32919  cnzh  32950  rezh  32951  dmvlsiga  33127  eulerpartgbij  33371  hgt750lemd  33660  hgt750lem  33663  hgt750lemb  33668  hgt750leme  33670  dnizeq0  35351  cnndvlem1  35413  taupi  36204  poimirlem28  36516  poimirlem31  36519  poimirlem32  36520  asindmre  36571  areacirc  36581  ishlatiN  38225  gcdaddmzz2nni  40860  lcmeprodgcdi  40872  3lexlogpow5ineq1  40919  3lexlogpow2ineq1  40923  rabren3dioph  41553  oaomoencom  42067  inductionexd  42906  lhe4.4ex1a  43088  stoweidlem13  44729  stoweidlem26  44742  stoweidlem34  44750  stoweid  44779  wallispilem2  44782  fourierdlem62  44884  fourierdlem103  44925  fouriersw  44947  salexct3  45058  salgensscntex  45060  smfmullem4  45510  pldofph  45655  31prm  46265  9fppr8  46405  6gbe  46439  8gbe  46441  9gbo  46442  11gbo  46443  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  nnsum4primeseven  46468  tgblthelfgott  46483  tgoldbach  46485  zlmodzxzldeplem3  47183  zlmodzxzldep  47185  blennnt2  47275  fv2arycl  47334  2arymptfv  47336  line2  47438  line2x  47440  line2y  47441