Theorem 3pm3.2i 1358

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

Syntax hints:   ∧ wa 400   ∧ w3a 1103

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 1105

This theorem is referenced by:  mpbir3an  1360  3jaoiOLD  1455  ftp  7156  on2recsov  8655  hartogslem1  9505  cantnflem3  9661  cantnflem4  9662  trcl  9698  ttukeylem7  10500  f13idfv  14038  faclbnd4lem1  14331  4bc2eq6  14367  hashge3el3dif  14526  hash3tpb  14534  funcnvs3  14953  wrdl3s3  15001  infcvgaux1i  15913  halfleoddlt  16421  strleun  17218  strle1  17219  slotstnscsi  17414  slotsdnscsi  17446  slotsdifunifndx  17455  slotsbhcdif  17469  setc2obas  18152  estrres  18196  srgbinomlem4  20312  cnfldfunALT  21518  xrsnsgrp  21539  psrass1  22094  psrass23l  22097  psrass23  22099  mplsubrg  22135  mplmon  22167  mplmonmul  22168  mplcoe1  22169  mplbas2  22174  evlslem2  22211  coe1mul2  22411  zfbas  24034  ust0  24358  utop2nei  24388  isclmi0  25238  iscvsi  25269  plypf1  26350  1cubr  26985  birthdaylem1  27094  divsqrtsumlem  27122  lgslem2  27440  lgsdir2lem2  27468  lgsdir2lem3  27469  addsqn2reu  27583  addsqrexnreu  27584  addsqnreup  27585  nolt02o  27837  nogt01o  27838  noinds  28116  norecov  28118  norec2ov  28128  bdayfinbndlem1  28638  axlowdimlem6  29275  usgrexmpldifpr  29586  0grsubgr  29606  upgrewlkle2  29934  usgr2wlkspthlem2  30085  usgr2pthlem  30090  elwspths2spth  30297  wlk2v2e  30486  ntrl2v2e  30487  konigsberglem4  30584  konigsberglem5  30585  ex-dvds  30785  sspid  31055  lnocoi  31087  nmlno0lem  31123  nmblolbii  31129  blocnilem  31134  phpar  31154  ip0i  31155  ip2i  31158  ipdirilem  31159  ipasslem10  31169  ip2dii  31174  siilem1  31181  siilem2  31182  hhssabloilem  31591  hhsst  31596  hhsssh2  31600  fh1i  31951  fh2i  31952  cm2ji  31955  pjoi0i  32048  elunop2  32343  mdslle1i  32647  mdslle2i  32648  mdslj1i  32649  mdslj2i  32650  mdslmd1lem1  32655  mdslmd2i  32660  dp2lt  33182  dpadd3  33209  threehalves  33212  cyc3evpm  33448  xrge0slmod  33646  zringfrac  33822  psrmonmul  33918  cos9thpiminplylem5  34154  xrge0iifmhm  34307  cnzh  34336  rezh  34337  dmvlsiga  34497  eulerpartgbij  34740  hgt750lemd  35013  hgt750lem  35016  hgt750lemb  35021  hgt750leme  35023  tz9.1regs  35525  dnizeq0  37042  cnndvlem1  37104  taupi  37945  poimirlem28  38277  poimirlem31  38280  poimirlem32  38281  asindmre  38332  areacirc  38342  ishlatiN  40107  gcdaddmzz2nni  42739  lcmeprodgcdi  42752  3lexlogpow5ineq1  42799  3lexlogpow2ineq1  42803  rabren3dioph  43522  oaomoencom  44024  inductionexd  44861  lhe4.4ex1a  45019  stoweidlem13  46707  stoweidlem26  46720  stoweidlem34  46728  stoweid  46757  wallispilem2  46760  fourierdlem62  46862  fourierdlem103  46903  fouriersw  46925  salexct3  47036  salgensscntex  47038  smfmullem4  47488  pldofph  47659  31prm  48326  9fppr8  48479  6gbe  48513  8gbe  48515  9gbo  48516  11gbo  48517  nnsum4primesodd  48538  nnsum4primesoddALTV  48539  nnsum4primeseven  48542  tgblthelfgott  48557  tgoldbach  48559  usgrexmpl1lem  48763  usgrexmpl1tri  48767  usgrexmpl2lem  48768  gpg5grlim  48835  gpg5grlic  48836  gpgprismgr4cycllem2  48838  zlmodzxzldeplem3  49259  zlmodzxzldep  49261  blennnt2  49346  fv2arycl  49405  2arymptfv  49407  line2  49509  line2x  49511  line2y  49512  setc1onsubc  50357