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  7096  on2recsov  8589  hartogslem1  9435  cantnflem3  9588  cantnflem4  9589  trcl  9625  ttukeylem7  10413  f13idfv  13909  faclbnd4lem1  14202  4bc2eq6  14238  hashge3el3dif  14396  hash3tpb  14404  funcnvs3  14823  wrdl3s3  14871  infcvgaux1i  15766  halfleoddlt  16275  strleun  17070  strle1  17071  slotstnscsi  17266  slotsdnscsi  17298  slotsdifunifndx  17307  slotsbhcdif  17321  setc2obas  18003  estrres  18047  srgbinomlem4  20149  cnfldfunALT  21308  cnfldfunALTOLD  21321  xrsnsgrp  21346  psrass1  21902  psrass23l  21905  psrass23  21907  mplsubrg  21943  mplmon  21971  mplmonmul  21972  mplcoe1  21973  mplbas2  21978  evlslem2  22015  coe1mul2  22184  zfbas  23812  ust0  24136  utop2nei  24166  isclmi0  25026  iscvsi  25057  plypf1  26145  1cubr  26780  birthdaylem1  26889  divsqrtsumlem  26918  lgslem2  27237  lgsdir2lem2  27265  lgsdir2lem3  27266  addsqn2reu  27380  addsqrexnreu  27381  addsqnreup  27382  nolt02o  27635  nogt01o  27636  noinds  27889  norecov  27891  norec2ov  27901  axlowdimlem6  28927  usgrexmpldifpr  29238  0grsubgr  29258  upgrewlkle2  29587  usgr2wlkspthlem2  29738  usgr2pthlem  29743  elwspths2spth  29950  wlk2v2e  30139  ntrl2v2e  30140  konigsberglem4  30237  konigsberglem5  30238  ex-dvds  30438  sspid  30707  lnocoi  30739  nmlno0lem  30775  nmblolbii  30781  blocnilem  30786  phpar  30806  ip0i  30807  ip2i  30810  ipdirilem  30811  ipasslem10  30821  ip2dii  30826  siilem1  30833  siilem2  30834  hhssabloilem  31243  hhsst  31248  hhsssh2  31252  fh1i  31603  fh2i  31604  cm2ji  31607  pjoi0i  31700  elunop2  31995  mdslle1i  32299  mdslle2i  32300  mdslj1i  32301  mdslj2i  32302  mdslmd1lem1  32307  mdslmd2i  32312  dp2lt  32872  dpadd3  32899  threehalves  32902  cyc3evpm  33126  xrge0slmod  33320  zringfrac  33526  cos9thpiminplylem5  33820  xrge0iifmhm  33973  cnzh  34002  rezh  34003  dmvlsiga  34163  eulerpartgbij  34406  hgt750lemd  34682  hgt750lem  34685  hgt750lemb  34690  hgt750leme  34692  tz9.1regs  35151  dnizeq0  36540  cnndvlem1  36602  taupi  37388  poimirlem28  37708  poimirlem31  37711  poimirlem32  37712  asindmre  37763  areacirc  37773  ishlatiN  39474  gcdaddmzz2nni  42107  lcmeprodgcdi  42120  3lexlogpow5ineq1  42167  3lexlogpow2ineq1  42171  rabren3dioph  42932  oaomoencom  43434  inductionexd  44272  lhe4.4ex1a  44446  stoweidlem13  46135  stoweidlem26  46148  stoweidlem34  46156  stoweid  46185  wallispilem2  46188  fourierdlem62  46290  fourierdlem103  46331  fouriersw  46353  salexct3  46464  salgensscntex  46466  smfmullem4  46916  pldofph  47069  31prm  47721  9fppr8  47861  6gbe  47895  8gbe  47897  9gbo  47898  11gbo  47899  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  nnsum4primeseven  47924  tgblthelfgott  47939  tgoldbach  47941  usgrexmpl1lem  48145  usgrexmpl1tri  48149  usgrexmpl2lem  48150  gpg5grlim  48217  gpg5grlic  48218  gpgprismgr4cycllem2  48220  zlmodzxzldeplem3  48627  zlmodzxzldep  48629  blennnt2  48714  fv2arycl  48773  2arymptfv  48775  line2  48877  line2x  48879  line2y  48880  setc1onsubc  49727