Theorem 3pm3.2i 1341

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 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
6	3, 4, 5	mpbir2an 712	1 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Syntax hints:   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  mpbir3an  1343  3jaoi  1431  ftp  7112  on2recsov  8606  hartogslem1  9459  cantnflem3  9612  cantnflem4  9613  trcl  9649  ttukeylem7  10437  f13idfv  13935  faclbnd4lem1  14228  4bc2eq6  14264  hashge3el3dif  14422  hash3tpb  14430  funcnvs3  14849  wrdl3s3  14897  infcvgaux1i  15792  halfleoddlt  16301  strleun  17096  strle1  17097  slotstnscsi  17292  slotsdnscsi  17324  slotsdifunifndx  17333  slotsbhcdif  17347  setc2obas  18030  estrres  18074  srgbinomlem4  20176  cnfldfunALT  21336  cnfldfunALTOLD  21349  xrsnsgrp  21374  psrass1  21931  psrass23l  21934  psrass23  21936  mplsubrg  21972  mplmon  22002  mplmonmul  22003  mplcoe1  22004  mplbas2  22009  evlslem2  22046  coe1mul2  22223  zfbas  23852  ust0  24176  utop2nei  24206  isclmi0  25066  iscvsi  25097  plypf1  26185  1cubr  26820  birthdaylem1  26929  divsqrtsumlem  26958  lgslem2  27277  lgsdir2lem2  27305  lgsdir2lem3  27306  addsqn2reu  27420  addsqrexnreu  27421  addsqnreup  27422  nolt02o  27675  nogt01o  27676  noinds  27953  norecov  27955  norec2ov  27965  bdayfinbndlem1  28475  axlowdimlem6  29032  usgrexmpldifpr  29343  0grsubgr  29363  upgrewlkle2  29692  usgr2wlkspthlem2  29843  usgr2pthlem  29848  elwspths2spth  30055  wlk2v2e  30244  ntrl2v2e  30245  konigsberglem4  30342  konigsberglem5  30343  ex-dvds  30543  sspid  30812  lnocoi  30844  nmlno0lem  30880  nmblolbii  30886  blocnilem  30891  phpar  30911  ip0i  30912  ip2i  30915  ipdirilem  30916  ipasslem10  30926  ip2dii  30931  siilem1  30938  siilem2  30939  hhssabloilem  31348  hhsst  31353  hhsssh2  31357  fh1i  31708  fh2i  31709  cm2ji  31712  pjoi0i  31805  elunop2  32100  mdslle1i  32404  mdslle2i  32405  mdslj1i  32406  mdslj2i  32407  mdslmd1lem1  32412  mdslmd2i  32417  dp2lt  32976  dpadd3  33003  threehalves  33006  cyc3evpm  33243  xrge0slmod  33440  zringfrac  33646  psrmonmul  33726  cos9thpiminplylem5  33963  xrge0iifmhm  34116  cnzh  34145  rezh  34146  dmvlsiga  34306  eulerpartgbij  34549  hgt750lemd  34825  hgt750lem  34828  hgt750lemb  34833  hgt750leme  34835  tz9.1regs  35309  dnizeq0  36694  cnndvlem1  36756  taupi  37572  poimirlem28  37893  poimirlem31  37896  poimirlem32  37897  asindmre  37948  areacirc  37958  ishlatiN  39725  gcdaddmzz2nni  42358  lcmeprodgcdi  42371  3lexlogpow5ineq1  42418  3lexlogpow2ineq1  42422  rabren3dioph  43166  oaomoencom  43668  inductionexd  44505  lhe4.4ex1a  44679  stoweidlem13  46365  stoweidlem26  46378  stoweidlem34  46386  stoweid  46415  wallispilem2  46418  fourierdlem62  46520  fourierdlem103  46561  fouriersw  46583  salexct3  46694  salgensscntex  46696  smfmullem4  47146  pldofph  47299  31prm  47951  9fppr8  48091  6gbe  48125  8gbe  48127  9gbo  48128  11gbo  48129  nnsum4primesodd  48150  nnsum4primesoddALTV  48151  nnsum4primeseven  48154  tgblthelfgott  48169  tgoldbach  48171  usgrexmpl1lem  48375  usgrexmpl1tri  48379  usgrexmpl2lem  48380  gpg5grlim  48447  gpg5grlic  48448  gpgprismgr4cycllem2  48450  zlmodzxzldeplem3  48856  zlmodzxzldep  48858  blennnt2  48943  fv2arycl  49002  2arymptfv  49004  line2  49106  line2x  49108  line2y  49109  setc1onsubc  49955