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 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  1342  3jaoi  1430  ftp  7102  on2recsov  8596  hartogslem1  9447  cantnflem3  9600  cantnflem4  9601  trcl  9637  ttukeylem7  10425  f13idfv  13923  faclbnd4lem1  14216  4bc2eq6  14252  hashge3el3dif  14410  hash3tpb  14418  funcnvs3  14837  wrdl3s3  14885  infcvgaux1i  15780  halfleoddlt  16289  strleun  17084  strle1  17085  slotstnscsi  17280  slotsdnscsi  17312  slotsdifunifndx  17321  slotsbhcdif  17335  setc2obas  18018  estrres  18062  srgbinomlem4  20164  cnfldfunALT  21324  cnfldfunALTOLD  21337  xrsnsgrp  21362  psrass1  21919  psrass23l  21922  psrass23  21924  mplsubrg  21960  mplmon  21990  mplmonmul  21991  mplcoe1  21992  mplbas2  21997  evlslem2  22034  coe1mul2  22211  zfbas  23840  ust0  24164  utop2nei  24194  isclmi0  25054  iscvsi  25085  plypf1  26173  1cubr  26808  birthdaylem1  26917  divsqrtsumlem  26946  lgslem2  27265  lgsdir2lem2  27293  lgsdir2lem3  27294  addsqn2reu  27408  addsqrexnreu  27409  addsqnreup  27410  nolt02o  27663  nogt01o  27664  noinds  27941  norecov  27943  norec2ov  27953  bdayfinbndlem1  28463  axlowdimlem6  29020  usgrexmpldifpr  29331  0grsubgr  29351  upgrewlkle2  29680  usgr2wlkspthlem2  29831  usgr2pthlem  29836  elwspths2spth  30043  wlk2v2e  30232  ntrl2v2e  30233  konigsberglem4  30330  konigsberglem5  30331  ex-dvds  30531  sspid  30800  lnocoi  30832  nmlno0lem  30868  nmblolbii  30874  blocnilem  30879  phpar  30899  ip0i  30900  ip2i  30903  ipdirilem  30904  ipasslem10  30914  ip2dii  30919  siilem1  30926  siilem2  30927  hhssabloilem  31336  hhsst  31341  hhsssh2  31345  fh1i  31696  fh2i  31697  cm2ji  31700  pjoi0i  31793  elunop2  32088  mdslle1i  32392  mdslle2i  32393  mdslj1i  32394  mdslj2i  32395  mdslmd1lem1  32400  mdslmd2i  32405  dp2lt  32966  dpadd3  32993  threehalves  32996  cyc3evpm  33232  xrge0slmod  33429  zringfrac  33635  cos9thpiminplylem5  33943  xrge0iifmhm  34096  cnzh  34125  rezh  34126  dmvlsiga  34286  eulerpartgbij  34529  hgt750lemd  34805  hgt750lem  34808  hgt750lemb  34813  hgt750leme  34815  tz9.1regs  35290  dnizeq0  36675  cnndvlem1  36737  taupi  37524  poimirlem28  37845  poimirlem31  37848  poimirlem32  37849  asindmre  37900  areacirc  37910  ishlatiN  39611  gcdaddmzz2nni  42244  lcmeprodgcdi  42257  3lexlogpow5ineq1  42304  3lexlogpow2ineq1  42308  rabren3dioph  43053  oaomoencom  43555  inductionexd  44392  lhe4.4ex1a  44566  stoweidlem13  46253  stoweidlem26  46266  stoweidlem34  46274  stoweid  46303  wallispilem2  46306  fourierdlem62  46408  fourierdlem103  46449  fouriersw  46471  salexct3  46582  salgensscntex  46584  smfmullem4  47034  pldofph  47187  31prm  47839  9fppr8  47979  6gbe  48013  8gbe  48015  9gbo  48016  11gbo  48017  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  nnsum4primeseven  48042  tgblthelfgott  48057  tgoldbach  48059  usgrexmpl1lem  48263  usgrexmpl1tri  48267  usgrexmpl2lem  48268  gpg5grlim  48335  gpg5grlic  48336  gpgprismgr4cycllem2  48338  zlmodzxzldeplem3  48744  zlmodzxzldep  48746  blennnt2  48831  fv2arycl  48890  2arymptfv  48892  line2  48994  line2x  48996  line2y  48997  setc1onsubc  49843