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 476	. 2 ⊢ (𝜑 ∧ 𝜓)
4		3pm3.2i.3	. 2 ⊢ 𝜒
5		df-3an 1105	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
6	3, 4, 5	mpbir2an 724	1 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

This proof depends on syntax axioms:   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mpbir3an  1360  3jaoiOLD  1455  ftp  7155  on2recsov  8659  hartogslem1  9517  cantnflem3  9673  cantnflem4  9674  trcl  9710  ttukeylem7  10520  f13idfv  14067  faclbnd4lem1  14360  4bc2eq6  14396  hashge3el3dif  14555  hash3tpb  14563  funcnvs3  14988  wrdl3s3  15038  infcvgaux1i  15949  halfleoddlt  16455  strleun  17252  strle1  17253  slotstnscsi  17448  slotsdnscsi  17480  slotsdifunifndx  17489  slotsbhcdif  17503  setc2obas  18186  estrres  18230  srgbinomlem4  20371  cnfldfunALT  21603  xrsnsgrp  21624  psrass1  22181  psrass23l  22184  psrass23  22186  mplsubrg  22222  mplmon  22254  mplmonmul  22255  mplcoe1  22256  mplbas2  22261  evlslem2  22298  coe1mul2  22498  zfbas  24125  ust0  24449  utop2nei  24479  isclmi0  25329  iscvsi  25360  plypf1  26441  1cubr  27082  birthdaylem1  27191  divsqrtsumlem  27219  lgslem2  27537  lgsdir2lem2  27565  lgsdir2lem3  27566  addsqn2reu  27680  addsqrexnreu  27681  addsqnreup  27682  nolt02o  27934  nogt01o  27935  noinds  28213  norecov  28215  norec2ov  28225  bdayfinbndlem1  28735  axlowdimlem6  29407  usgrexmpldifpr  29721  0grsubgr  29741  upgrewlkle2  30069  usgr2wlkspthlem2  30226  usgr2pthlem  30231  elwspths2spth  30441  wlk2v2e  30640  ntrl2v2e  30641  konigsberglem4  30738  konigsberglem5  30739  ex-dvds  30939  sspid  31209  lnocoi  31241  nmlno0lem  31277  nmblolbii  31283  blocnilem  31288  phpar  31308  ip0i  31309  ip2i  31312  ipdirilem  31313  ipasslem10  31323  ip2dii  31328  siilem1  31335  siilem2  31336  hhssabloilem  31745  hhsst  31750  hhsssh2  31754  fh1i  32105  fh2i  32106  cm2ji  32109  pjoi0i  32202  elunop2  32497  mdslle1i  32801  mdslle2i  32802  mdslj1i  32803  mdslj2i  32804  mdslmd1lem1  32809  mdslmd2i  32814  dp2lt  33333  dpadd3  33360  threehalves  33363  cyc3evpm  33593  xrge0slmod  33791  zringfrac  33967  psrmonmul  34063  cos9thpiminplylem5  34299  xrge0iifmhm  34452  cnzh  34481  rezh  34482  dmvlsiga  34642  eulerpartgbij  34886  hgt750lemd  35159  hgt750lem  35162  hgt750lemb  35167  hgt750leme  35169  tz9.1regs  35663  dnizeq0  37175  cnndvlem1  37237  taupi  38078  poimirlem28  38400  poimirlem31  38403  poimirlem32  38404  asindmre  38455  areacirc  38465  ishlatiN  40231  gcdaddmzz2nni  42863  lcmeprodgcdi  42876  3lexlogpow5ineq1  42923  3lexlogpow2ineq1  42927  rabren3dioph  43659  oaomoencom  44161  inductionexd  44998  lhe4.4ex1a  45156  stoweidlem13  46844  stoweidlem26  46857  stoweidlem34  46865  stoweid  46894  wallispilem2  46897  fourierdlem62  46999  fourierdlem103  47040  fouriersw  47062  salexct3  47173  salgensscntex  47175  smfmullem4  47625  pldofph  47836  31prm  48503  9fppr8  48656  6gbe  48690  8gbe  48692  9gbo  48693  11gbo  48694  nnsum4primesodd  48715  nnsum4primesoddALTV  48716  nnsum4primeseven  48719  tgblthelfgott  48734  tgoldbach  48736  usgrexmpl1lem  48940  usgrexmpl1tri  48944  usgrexmpl2lem  48945  gpg5grlim  49012  gpg5grlic  49013  gpgprismgr4cycllem2  49015  zlmodzxzldeplem3  49435  zlmodzxzldep  49437  blennnt2  49522  fv2arycl  49581  2arymptfv  49583  line2  49685  line2x  49687  line2y  49688  setc1onsubc  50531  crosspdotsumlem  50800