Theorem 3pm3.2i 1339

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

Syntax hints:   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  mpbir3an  1341  3jaoi  1427  ftp  7157  on2recsov  8669  hartogslem1  9539  cantnflem3  9688  cantnflem4  9689  trcl  9725  ttukeylem7  10512  f13idfv  13969  faclbnd4lem1  14257  4bc2eq6  14293  hashge3el3dif  14451  funcnvs3  14869  wrdl3s3  14917  infcvgaux1i  15807  halfleoddlt  16309  strleun  17094  strle1  17095  slotstnscsi  17309  slotsdnscsi  17341  slotsdifunifndx  17350  slotsbhcdif  17364  slotsbhcdifOLD  17365  setc2obas  18048  estrres  18095  srgbinomlem4  20123  cnfldfunALT  21157  cnfldfunALTOLD  21158  xrsnsgrp  21181  psrass1  21744  psrass23l  21747  psrass23  21749  mplsubrg  21783  mplmon  21809  mplmonmul  21810  mplcoe1  21811  mplbas2  21816  evlslem2  21861  coe1mul2  22011  zfbas  23620  ust0  23944  utop2nei  23975  isclmi0  24838  iscvsi  24869  plypf1  25950  1cubr  26571  birthdaylem1  26680  divsqrtsumlem  26708  lgslem2  27025  lgsdir2lem2  27053  lgsdir2lem3  27054  addsqn2reu  27168  addsqrexnreu  27169  addsqnreup  27170  nolt02o  27422  nogt01o  27423  noinds  27655  norecov  27657  norec2ov  27667  axlowdimlem6  28460  usgrexmpldifpr  28770  0grsubgr  28790  upgrewlkle2  29118  usgr2wlkspthlem2  29270  usgr2pthlem  29275  elwspths2spth  29476  wlk2v2e  29665  ntrl2v2e  29666  konigsberglem4  29763  konigsberglem5  29764  ex-dvds  29964  sspid  30233  lnocoi  30265  nmlno0lem  30301  nmblolbii  30307  blocnilem  30312  phpar  30332  ip0i  30333  ip2i  30336  ipdirilem  30337  ipasslem10  30347  ip2dii  30352  siilem1  30359  siilem2  30360  hhssabloilem  30769  hhsst  30774  hhsssh2  30778  fh1i  31129  fh2i  31130  cm2ji  31133  pjoi0i  31226  elunop2  31521  mdslle1i  31825  mdslle2i  31826  mdslj1i  31827  mdslj2i  31828  mdslmd1lem1  31833  mdslmd2i  31838  dp2lt  32306  dpadd3  32333  threehalves  32336  cyc3evpm  32567  xrge0slmod  32721  xrge0iifmhm  33205  cnzh  33236  rezh  33237  dmvlsiga  33413  eulerpartgbij  33657  hgt750lemd  33946  hgt750lem  33949  hgt750lemb  33954  hgt750leme  33956  gg-cnfldfunALT  35484  dnizeq0  35654  cnndvlem1  35716  taupi  36507  poimirlem28  36819  poimirlem31  36822  poimirlem32  36823  asindmre  36874  areacirc  36884  ishlatiN  38528  gcdaddmzz2nni  41166  lcmeprodgcdi  41178  3lexlogpow5ineq1  41225  3lexlogpow2ineq1  41229  rabren3dioph  41855  oaomoencom  42369  inductionexd  43208  lhe4.4ex1a  43390  stoweidlem13  45028  stoweidlem26  45041  stoweidlem34  45049  stoweid  45078  wallispilem2  45081  fourierdlem62  45183  fourierdlem103  45224  fouriersw  45246  salexct3  45357  salgensscntex  45359  smfmullem4  45809  pldofph  45954  31prm  46564  9fppr8  46704  6gbe  46738  8gbe  46740  9gbo  46741  11gbo  46742  nnsum4primesodd  46763  nnsum4primesoddALTV  46764  nnsum4primeseven  46767  tgblthelfgott  46782  tgoldbach  46784  zlmodzxzldeplem3  47271  zlmodzxzldep  47273  blennnt2  47363  fv2arycl  47422  2arymptfv  47424  line2  47526  line2x  47528  line2y  47529