Theorem 3pm3.2i 1338

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

Syntax hints:   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  mpbir3an  1340  3jaoi  1427  ftp  7176  on2recsov  8704  hartogslem1  9579  cantnflem3  9728  cantnflem4  9729  trcl  9765  ttukeylem7  10552  f13idfv  14037  faclbnd4lem1  14328  4bc2eq6  14364  hashge3el3dif  14522  hash3tpb  14530  funcnvs3  14949  wrdl3s3  14997  infcvgaux1i  15889  halfleoddlt  16395  strleun  17190  strle1  17191  slotstnscsi  17405  slotsdnscsi  17437  slotsdifunifndx  17446  slotsbhcdif  17460  slotsbhcdifOLD  17461  setc2obas  18147  estrres  18194  srgbinomlem4  20246  cnfldfunALT  21396  cnfldfunALTOLD  21409  cnfldfunALTOLDOLD  21410  xrsnsgrp  21437  psrass1  22001  psrass23l  22004  psrass23  22006  mplsubrg  22042  mplmon  22070  mplmonmul  22071  mplcoe1  22072  mplbas2  22077  evlslem2  22120  coe1mul2  22287  zfbas  23919  ust0  24243  utop2nei  24274  isclmi0  25144  iscvsi  25175  plypf1  26265  1cubr  26899  birthdaylem1  27008  divsqrtsumlem  27037  lgslem2  27356  lgsdir2lem2  27384  lgsdir2lem3  27385  addsqn2reu  27499  addsqrexnreu  27500  addsqnreup  27501  nolt02o  27754  nogt01o  27755  noinds  27992  norecov  27994  norec2ov  28004  nohalf  28421  axlowdimlem6  28976  usgrexmpldifpr  29289  0grsubgr  29309  upgrewlkle2  29638  usgr2wlkspthlem2  29790  usgr2pthlem  29795  elwspths2spth  29996  wlk2v2e  30185  ntrl2v2e  30186  konigsberglem4  30283  konigsberglem5  30284  ex-dvds  30484  sspid  30753  lnocoi  30785  nmlno0lem  30821  nmblolbii  30827  blocnilem  30832  phpar  30852  ip0i  30853  ip2i  30856  ipdirilem  30857  ipasslem10  30867  ip2dii  30872  siilem1  30879  siilem2  30880  hhssabloilem  31289  hhsst  31294  hhsssh2  31298  fh1i  31649  fh2i  31650  cm2ji  31653  pjoi0i  31746  elunop2  32041  mdslle1i  32345  mdslle2i  32346  mdslj1i  32347  mdslj2i  32348  mdslmd1lem1  32353  mdslmd2i  32358  dp2lt  32851  dpadd3  32878  threehalves  32881  cyc3evpm  33152  xrge0slmod  33355  zringfrac  33561  xrge0iifmhm  33899  cnzh  33930  rezh  33931  dmvlsiga  34109  eulerpartgbij  34353  hgt750lemd  34641  hgt750lem  34644  hgt750lemb  34649  hgt750leme  34651  dnizeq0  36457  cnndvlem1  36519  taupi  37305  poimirlem28  37634  poimirlem31  37637  poimirlem32  37638  asindmre  37689  areacirc  37699  ishlatiN  39336  gcdaddmzz2nni  41975  lcmeprodgcdi  41988  3lexlogpow5ineq1  42035  3lexlogpow2ineq1  42039  rabren3dioph  42802  oaomoencom  43306  inductionexd  44144  lhe4.4ex1a  44324  stoweidlem13  45968  stoweidlem26  45981  stoweidlem34  45989  stoweid  46018  wallispilem2  46021  fourierdlem62  46123  fourierdlem103  46164  fouriersw  46186  salexct3  46297  salgensscntex  46299  smfmullem4  46749  pldofph  46894  31prm  47521  9fppr8  47661  6gbe  47695  8gbe  47697  9gbo  47698  11gbo  47699  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  tgblthelfgott  47739  tgoldbach  47741  usgrexmpl1lem  47915  usgrexmpl1tri  47919  usgrexmpl2lem  47920  gpg5grlic  47974  zlmodzxzldeplem3  48347  zlmodzxzldep  48349  blennnt2  48438  fv2arycl  48497  2arymptfv  48499  line2  48601  line2x  48603  line2y  48604