Theorem 3pm3.2i 1346

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

Syntax hints:   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  mpbir3an  1348  3jaoi  1436  ftp  7107  on2recsov  8601  hartogslem1  9454  cantnflem3  9610  cantnflem4  9611  trcl  9647  ttukeylem7  10435  f13idfv  13960  faclbnd4lem1  14253  4bc2eq6  14289  hashge3el3dif  14447  hash3tpb  14455  funcnvs3  14874  wrdl3s3  14922  infcvgaux1i  15820  halfleoddlt  16329  strleun  17125  strle1  17126  slotstnscsi  17321  slotsdnscsi  17353  slotsdifunifndx  17362  slotsbhcdif  17376  setc2obas  18059  estrres  18103  srgbinomlem4  20208  cnfldfunALT  21369  xrsnsgrp  21390  psrass1  21945  psrass23l  21948  psrass23  21950  mplsubrg  21986  mplmon  22018  mplmonmul  22019  mplcoe1  22020  mplbas2  22025  evlslem2  22062  coe1mul2  22262  zfbas  23886  ust0  24210  utop2nei  24240  isclmi0  25090  iscvsi  25121  plypf1  26202  1cubr  26831  birthdaylem1  26940  divsqrtsumlem  26968  lgslem2  27286  lgsdir2lem2  27314  lgsdir2lem3  27315  addsqn2reu  27429  addsqrexnreu  27430  addsqnreup  27431  nolt02o  27684  nogt01o  27685  noinds  27962  norecov  27964  norec2ov  27974  bdayfinbndlem1  28484  axlowdimlem6  29041  usgrexmpldifpr  29352  0grsubgr  29372  upgrewlkle2  29700  usgr2wlkspthlem2  29851  usgr2pthlem  29856  elwspths2spth  30063  wlk2v2e  30252  ntrl2v2e  30253  konigsberglem4  30350  konigsberglem5  30351  ex-dvds  30551  sspid  30821  lnocoi  30853  nmlno0lem  30889  nmblolbii  30895  blocnilem  30900  phpar  30920  ip0i  30921  ip2i  30924  ipdirilem  30925  ipasslem10  30935  ip2dii  30940  siilem1  30947  siilem2  30948  hhssabloilem  31357  hhsst  31362  hhsssh2  31366  fh1i  31717  fh2i  31718  cm2ji  31721  pjoi0i  31814  elunop2  32109  mdslle1i  32413  mdslle2i  32414  mdslj1i  32415  mdslj2i  32416  mdslmd1lem1  32421  mdslmd2i  32426  dp2lt  32970  dpadd3  32997  threehalves  33000  cyc3evpm  33238  xrge0slmod  33438  zringfrac  33644  psrmonmul  33741  cos9thpiminplylem5  33977  xrge0iifmhm  34130  cnzh  34159  rezh  34160  dmvlsiga  34320  eulerpartgbij  34563  hgt750lemd  34839  hgt750lem  34842  hgt750lemb  34847  hgt750leme  34849  tz9.1regs  35322  dnizeq0  36788  cnndvlem1  36850  taupi  37690  poimirlem28  38022  poimirlem31  38025  poimirlem32  38026  asindmre  38077  areacirc  38087  ishlatiN  39854  gcdaddmzz2nni  42486  lcmeprodgcdi  42499  3lexlogpow5ineq1  42546  3lexlogpow2ineq1  42550  rabren3dioph  43267  oaomoencom  43769  inductionexd  44606  lhe4.4ex1a  44780  stoweidlem13  46463  stoweidlem26  46476  stoweidlem34  46484  stoweid  46513  wallispilem2  46516  fourierdlem62  46618  fourierdlem103  46659  fouriersw  46681  salexct3  46792  salgensscntex  46794  smfmullem4  47244  pldofph  47415  31prm  48082  9fppr8  48235  6gbe  48269  8gbe  48271  9gbo  48272  11gbo  48273  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  nnsum4primeseven  48298  tgblthelfgott  48313  tgoldbach  48315  usgrexmpl1lem  48519  usgrexmpl1tri  48523  usgrexmpl2lem  48524  gpg5grlim  48591  gpg5grlic  48592  gpgprismgr4cycllem2  48594  zlmodzxzldeplem3  49000  zlmodzxzldep  49002  blennnt2  49087  fv2arycl  49146  2arymptfv  49148  line2  49250  line2x  49252  line2y  49253  setc1onsubc  50099