Theorem 3pm3.2i 1352

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

Syntax hints:   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  mpbir3an  1354  3jaoiOLD  1447  ftp  7136  on2recsov  8633  hartogslem1  9487  cantnflem3  9643  cantnflem4  9644  trcl  9680  ttukeylem7  10469  f13idfv  14010  faclbnd4lem1  14303  4bc2eq6  14339  hashge3el3dif  14497  hash3tpb  14505  funcnvs3  14924  wrdl3s3  14972  infcvgaux1i  15870  halfleoddlt  16379  strleun  17176  strle1  17177  slotstnscsi  17372  slotsdnscsi  17404  slotsdifunifndx  17413  slotsbhcdif  17427  setc2obas  18110  estrres  18154  srgbinomlem4  20258  cnfldfunALT  21419  xrsnsgrp  21440  psrass1  21995  psrass23l  21998  psrass23  22000  mplsubrg  22036  mplmon  22068  mplmonmul  22069  mplcoe1  22070  mplbas2  22075  evlslem2  22112  coe1mul2  22312  zfbas  23936  ust0  24260  utop2nei  24290  isclmi0  25140  iscvsi  25171  plypf1  26252  1cubr  26884  birthdaylem1  26993  divsqrtsumlem  27021  lgslem2  27339  lgsdir2lem2  27367  lgsdir2lem3  27368  addsqn2reu  27482  addsqrexnreu  27483  addsqnreup  27484  nolt02o  27736  nogt01o  27737  noinds  28015  norecov  28017  norec2ov  28027  bdayfinbndlem1  28537  axlowdimlem6  29094  usgrexmpldifpr  29405  0grsubgr  29425  upgrewlkle2  29753  usgr2wlkspthlem2  29904  usgr2pthlem  29909  elwspths2spth  30116  wlk2v2e  30305  ntrl2v2e  30306  konigsberglem4  30403  konigsberglem5  30404  ex-dvds  30604  sspid  30874  lnocoi  30906  nmlno0lem  30942  nmblolbii  30948  blocnilem  30953  phpar  30973  ip0i  30974  ip2i  30977  ipdirilem  30978  ipasslem10  30988  ip2dii  30993  siilem1  31000  siilem2  31001  hhssabloilem  31410  hhsst  31415  hhsssh2  31419  fh1i  31770  fh2i  31771  cm2ji  31774  pjoi0i  31867  elunop2  32162  mdslle1i  32466  mdslle2i  32467  mdslj1i  32468  mdslj2i  32469  mdslmd1lem1  32474  mdslmd2i  32479  dp2lt  33023  dpadd3  33050  threehalves  33053  cyc3evpm  33291  xrge0slmod  33495  zringfrac  33711  psrmonmul  33808  cos9thpiminplylem5  34044  xrge0iifmhm  34197  cnzh  34226  rezh  34227  dmvlsiga  34387  eulerpartgbij  34630  hgt750lemd  34906  hgt750lem  34909  hgt750lemb  34914  hgt750leme  34916  tz9.1regs  35394  dnizeq0  36877  cnndvlem1  36939  taupi  37779  poimirlem28  38111  poimirlem31  38114  poimirlem32  38115  asindmre  38166  areacirc  38176  ishlatiN  39943  gcdaddmzz2nni  42575  lcmeprodgcdi  42588  3lexlogpow5ineq1  42635  3lexlogpow2ineq1  42639  rabren3dioph  43356  oaomoencom  43858  inductionexd  44695  lhe4.4ex1a  44869  stoweidlem13  46551  stoweidlem26  46564  stoweidlem34  46572  stoweid  46601  wallispilem2  46604  fourierdlem62  46706  fourierdlem103  46747  fouriersw  46769  salexct3  46880  salgensscntex  46882  smfmullem4  47332  pldofph  47503  31prm  48170  9fppr8  48323  6gbe  48357  8gbe  48359  9gbo  48360  11gbo  48361  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  nnsum4primeseven  48386  tgblthelfgott  48401  tgoldbach  48403  usgrexmpl1lem  48607  usgrexmpl1tri  48611  usgrexmpl2lem  48612  gpg5grlim  48679  gpg5grlic  48680  gpgprismgr4cycllem2  48682  zlmodzxzldeplem3  49088  zlmodzxzldep  49090  blennnt2  49175  fv2arycl  49234  2arymptfv  49236  line2  49338  line2x  49340  line2y  49341  setc1onsubc  50187