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  1456  brcoi  5853  ftp  7185  on2recsov  8705  hartogslem1  9563  cantnflem3  9719  cantnflem4  9720  trcl  9756  ttukeylem7  10620  f13idfv  14170  faclbnd4lem1  14464  4bc2eq6  14500  hashge3el3dif  14659  hash3tpb  14667  funcnvs3  15094  wrdl3s3  15144  infcvgaux1i  16055  halfleoddlt  16561  strleun  17364  strle1  17365  slotstnscsi  17560  slotsdnscsi  17592  slotsdifunifndx  17601  slotsbhcdif  17615  setc2obas  18298  estrres  18342  srgbinomlem4  20485  cnfldfunALT  21723  xrsnsgrp  21744  psrass1  22301  psrass23l  22304  psrass23  22306  mplsubrg  22342  mplmon  22374  mplmonmul  22375  mplcoe1  22376  mplbas2  22381  evlslem2  22418  coe1mul2  22618  zfbas  24245  ust0  24569  isclmi0  25449  iscvsi  25480  plypf1  26561  1cubr  27200  birthdaylem1  27309  divsqrtsumlem  27337  lgslem2  27655  lgsdir2lem2  27683  lgsdir2lem3  27684  addsqn2reu  27798  addsqrexnreu  27799  addsqnreup  27800  nolt02o  28082  nogt01o  28083  noinds  28361  norecov  28363  norec2ov  28373  bdayfinbndlem1  28883  axlowdimlem6  29555  usgrexmpldifpr  29869  0grsubgr  29889  upgrewlkle2  30217  usgr2wlkspthlem2  30374  usgr2pthlem  30379  elwspths2spth  30589  wlk2v2e  30788  ntrl2v2e  30789  konigsberglem4  30886  konigsberglem5  30887  ex-dvds  31087  sspid  31357  lnocoi  31389  nmlno0lem  31425  nmblolbii  31431  blocnilem  31436  phpar  31456  ip0i  31457  ip2i  31460  ipdirilem  31461  ipasslem10  31471  ip2dii  31476  siilem1  31483  siilem2  31484  hhssabloilem  31893  hhsst  31898  hhsssh2  31902  fh1i  32253  fh2i  32254  cm2ji  32257  pjoi0i  32350  elunop2  32645  mdslle1i  32949  mdslle2i  32950  mdslj1i  32951  mdslj2i  32952  mdslmd1lem1  32957  mdslmd2i  32962  dp2lt  33521  dpadd3  33548  threehalves  33551  cyc3evpm  33781  xrge0slmod  33979  zringfrac  34156  psrmonmul  34252  cos9thpiminplylem5  34488  xrge0iifmhm  34641  cnzh  34670  rezh  34671  dmvlsiga  34831  eulerpartgbij  35074  hgt750lemd  35347  hgt750lem  35350  hgt750lemb  35355  hgt750leme  35357  tz9.1regs  35902  dfk12  36012  dfk22  36013  dfk32  36014  dnizeq0  37519  cnndvlem1  37581  taupi  38436  poimirlem28  38758  poimirlem31  38761  poimirlem32  38762  asindmre  38813  areacirc  38823  ishlatiN  40604  gcdaddmzz2nni  43236  lcmeprodgcdi  43249  3lexlogpow5ineq1  43296  3lexlogpow2ineq1  43300  rabren3dioph  44015  oaomoencom  44511  inductionexd  45347  lhe4.4ex1a  45505  stoweidlem13  47228  stoweidlem26  47241  stoweidlem34  47249  stoweid  47278  wallispilem2  47281  fourierdlem62  47383  fourierdlem103  47424  fouriersw  47446  salexct3  47557  salgensscntex  47559  smfmullem4  48009  pldofph  48220  31prm  48887  9fppr8  49040  6gbe  49074  8gbe  49076  9gbo  49077  11gbo  49078  nnsum4primesodd  49099  nnsum4primesoddALTV  49100  nnsum4primeseven  49103  tgblthelfgott  49118  tgoldbach  49120  usgrexmpl1lem  49324  usgrexmpl1tri  49328  usgrexmpl2lem  49329  gpg5grlim  49396  gpg5grlic  49397  gpgprismgr4cycllem2  49399  zlmodzxzldeplem3  49819  zlmodzxzldep  49821  blennnt2  49906  fv2arycl  49965  2arymptfv  49967  setc1onsubc  50945  par2str  50974  parswapprop  50982  par2hom  50984  crosspdotsumlem  51244