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  7129  on2recsov  8632  hartogslem1  9495  cantnflem3  9644  cantnflem4  9645  trcl  9681  ttukeylem7  10468  f13idfv  13965  faclbnd4lem1  14258  4bc2eq6  14294  hashge3el3dif  14452  hash3tpb  14460  funcnvs3  14880  wrdl3s3  14928  infcvgaux1i  15823  halfleoddlt  16332  strleun  17127  strle1  17128  slotstnscsi  17323  slotsdnscsi  17355  slotsdifunifndx  17364  slotsbhcdif  17378  setc2obas  18056  estrres  18100  srgbinomlem4  20138  cnfldfunALT  21279  cnfldfunALTOLD  21292  xrsnsgrp  21319  psrass1  21873  psrass23l  21876  psrass23  21878  mplsubrg  21914  mplmon  21942  mplmonmul  21943  mplcoe1  21944  mplbas2  21949  evlslem2  21986  coe1mul2  22155  zfbas  23783  ust0  24107  utop2nei  24138  isclmi0  24998  iscvsi  25029  plypf1  26117  1cubr  26752  birthdaylem1  26861  divsqrtsumlem  26890  lgslem2  27209  lgsdir2lem2  27237  lgsdir2lem3  27238  addsqn2reu  27352  addsqrexnreu  27353  addsqnreup  27354  nolt02o  27607  nogt01o  27608  noinds  27852  norecov  27854  norec2ov  27864  axlowdimlem6  28874  usgrexmpldifpr  29185  0grsubgr  29205  upgrewlkle2  29534  usgr2wlkspthlem2  29688  usgr2pthlem  29693  elwspths2spth  29897  wlk2v2e  30086  ntrl2v2e  30087  konigsberglem4  30184  konigsberglem5  30185  ex-dvds  30385  sspid  30654  lnocoi  30686  nmlno0lem  30722  nmblolbii  30728  blocnilem  30733  phpar  30753  ip0i  30754  ip2i  30757  ipdirilem  30758  ipasslem10  30768  ip2dii  30773  siilem1  30780  siilem2  30781  hhssabloilem  31190  hhsst  31195  hhsssh2  31199  fh1i  31550  fh2i  31551  cm2ji  31554  pjoi0i  31647  elunop2  31942  mdslle1i  32246  mdslle2i  32247  mdslj1i  32248  mdslj2i  32249  mdslmd1lem1  32254  mdslmd2i  32259  dp2lt  32805  dpadd3  32832  threehalves  32835  cyc3evpm  33107  xrge0slmod  33319  zringfrac  33525  cos9thpiminplylem5  33776  xrge0iifmhm  33929  cnzh  33958  rezh  33959  dmvlsiga  34119  eulerpartgbij  34363  hgt750lemd  34639  hgt750lem  34642  hgt750lemb  34647  hgt750leme  34649  dnizeq0  36463  cnndvlem1  36525  taupi  37311  poimirlem28  37642  poimirlem31  37645  poimirlem32  37646  asindmre  37697  areacirc  37707  ishlatiN  39348  gcdaddmzz2nni  41982  lcmeprodgcdi  41995  3lexlogpow5ineq1  42042  3lexlogpow2ineq1  42046  rabren3dioph  42803  oaomoencom  43306  inductionexd  44144  lhe4.4ex1a  44318  stoweidlem13  46011  stoweidlem26  46024  stoweidlem34  46032  stoweid  46061  wallispilem2  46064  fourierdlem62  46166  fourierdlem103  46207  fouriersw  46229  salexct3  46340  salgensscntex  46342  smfmullem4  46792  pldofph  46946  31prm  47598  9fppr8  47738  6gbe  47772  8gbe  47774  9gbo  47775  11gbo  47776  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  tgblthelfgott  47816  tgoldbach  47818  usgrexmpl1lem  48012  usgrexmpl1tri  48016  usgrexmpl2lem  48017  gpg5grlic  48084  gpgprismgr4cycllem2  48086  zlmodzxzldeplem3  48491  zlmodzxzldep  48493  blennnt2  48578  fv2arycl  48637  2arymptfv  48639  line2  48741  line2x  48743  line2y  48744  setc1onsubc  49591