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  7102  on2recsov  8596  hartogslem1  9447  cantnflem3  9600  cantnflem4  9601  trcl  9637  ttukeylem7  10425  f13idfv  13923  faclbnd4lem1  14216  4bc2eq6  14252  hashge3el3dif  14410  hash3tpb  14418  funcnvs3  14837  wrdl3s3  14885  infcvgaux1i  15780  halfleoddlt  16289  strleun  17084  strle1  17085  slotstnscsi  17280  slotsdnscsi  17312  slotsdifunifndx  17321  slotsbhcdif  17335  setc2obas  18018  estrres  18062  srgbinomlem4  20164  cnfldfunALT  21324  cnfldfunALTOLD  21337  xrsnsgrp  21362  psrass1  21919  psrass23l  21922  psrass23  21924  mplsubrg  21960  mplmon  21990  mplmonmul  21991  mplcoe1  21992  mplbas2  21997  evlslem2  22034  coe1mul2  22211  zfbas  23840  ust0  24164  utop2nei  24194  isclmi0  25054  iscvsi  25085  plypf1  26173  1cubr  26808  birthdaylem1  26917  divsqrtsumlem  26946  lgslem2  27265  lgsdir2lem2  27293  lgsdir2lem3  27294  addsqn2reu  27408  addsqrexnreu  27409  addsqnreup  27410  nolt02o  27663  nogt01o  27664  noinds  27941  norecov  27943  norec2ov  27953  bdayfinbndlem1  28463  axlowdimlem6  29020  usgrexmpldifpr  29331  0grsubgr  29351  upgrewlkle2  29680  usgr2wlkspthlem2  29831  usgr2pthlem  29836  elwspths2spth  30043  wlk2v2e  30232  ntrl2v2e  30233  konigsberglem4  30330  konigsberglem5  30331  ex-dvds  30531  sspid  30800  lnocoi  30832  nmlno0lem  30868  nmblolbii  30874  blocnilem  30879  phpar  30899  ip0i  30900  ip2i  30903  ipdirilem  30904  ipasslem10  30914  ip2dii  30919  siilem1  30926  siilem2  30927  hhssabloilem  31336  hhsst  31341  hhsssh2  31345  fh1i  31696  fh2i  31697  cm2ji  31700  pjoi0i  31793  elunop2  32088  mdslle1i  32392  mdslle2i  32393  mdslj1i  32394  mdslj2i  32395  mdslmd1lem1  32400  mdslmd2i  32405  dp2lt  32966  dpadd3  32993  threehalves  32996  cyc3evpm  33232  xrge0slmod  33429  zringfrac  33635  cos9thpiminplylem5  33943  xrge0iifmhm  34096  cnzh  34125  rezh  34126  dmvlsiga  34286  eulerpartgbij  34529  hgt750lemd  34805  hgt750lem  34808  hgt750lemb  34813  hgt750leme  34815  tz9.1regs  35290  dnizeq0  36675  cnndvlem1  36737  taupi  37528  poimirlem28  37849  poimirlem31  37852  poimirlem32  37853  asindmre  37904  areacirc  37914  ishlatiN  39615  gcdaddmzz2nni  42248  lcmeprodgcdi  42261  3lexlogpow5ineq1  42308  3lexlogpow2ineq1  42312  rabren3dioph  43057  oaomoencom  43559  inductionexd  44396  lhe4.4ex1a  44570  stoweidlem13  46257  stoweidlem26  46270  stoweidlem34  46278  stoweid  46307  wallispilem2  46310  fourierdlem62  46412  fourierdlem103  46453  fouriersw  46475  salexct3  46586  salgensscntex  46588  smfmullem4  47038  pldofph  47191  31prm  47843  9fppr8  47983  6gbe  48017  8gbe  48019  9gbo  48020  11gbo  48021  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  nnsum4primeseven  48046  tgblthelfgott  48061  tgoldbach  48063  usgrexmpl1lem  48267  usgrexmpl1tri  48271  usgrexmpl2lem  48272  gpg5grlim  48339  gpg5grlic  48340  gpgprismgr4cycllem2  48342  zlmodzxzldeplem3  48748  zlmodzxzldep  48750  blennnt2  48835  fv2arycl  48894  2arymptfv  48896  line2  48998  line2x  49000  line2y  49001  setc1onsubc  49847