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  7132  on2recsov  8635  hartogslem1  9502  cantnflem3  9651  cantnflem4  9652  trcl  9688  ttukeylem7  10475  f13idfv  13972  faclbnd4lem1  14265  4bc2eq6  14301  hashge3el3dif  14459  hash3tpb  14467  funcnvs3  14887  wrdl3s3  14935  infcvgaux1i  15830  halfleoddlt  16339  strleun  17134  strle1  17135  slotstnscsi  17330  slotsdnscsi  17362  slotsdifunifndx  17371  slotsbhcdif  17385  setc2obas  18063  estrres  18107  srgbinomlem4  20145  cnfldfunALT  21286  cnfldfunALTOLD  21299  xrsnsgrp  21326  psrass1  21880  psrass23l  21883  psrass23  21885  mplsubrg  21921  mplmon  21949  mplmonmul  21950  mplcoe1  21951  mplbas2  21956  evlslem2  21993  coe1mul2  22162  zfbas  23790  ust0  24114  utop2nei  24145  isclmi0  25005  iscvsi  25036  plypf1  26124  1cubr  26759  birthdaylem1  26868  divsqrtsumlem  26897  lgslem2  27216  lgsdir2lem2  27244  lgsdir2lem3  27245  addsqn2reu  27359  addsqrexnreu  27360  addsqnreup  27361  nolt02o  27614  nogt01o  27615  noinds  27859  norecov  27861  norec2ov  27871  axlowdimlem6  28881  usgrexmpldifpr  29192  0grsubgr  29212  upgrewlkle2  29541  usgr2wlkspthlem2  29695  usgr2pthlem  29700  elwspths2spth  29904  wlk2v2e  30093  ntrl2v2e  30094  konigsberglem4  30191  konigsberglem5  30192  ex-dvds  30392  sspid  30661  lnocoi  30693  nmlno0lem  30729  nmblolbii  30735  blocnilem  30740  phpar  30760  ip0i  30761  ip2i  30764  ipdirilem  30765  ipasslem10  30775  ip2dii  30780  siilem1  30787  siilem2  30788  hhssabloilem  31197  hhsst  31202  hhsssh2  31206  fh1i  31557  fh2i  31558  cm2ji  31561  pjoi0i  31654  elunop2  31949  mdslle1i  32253  mdslle2i  32254  mdslj1i  32255  mdslj2i  32256  mdslmd1lem1  32261  mdslmd2i  32266  dp2lt  32812  dpadd3  32839  threehalves  32842  cyc3evpm  33114  xrge0slmod  33326  zringfrac  33532  cos9thpiminplylem5  33783  xrge0iifmhm  33936  cnzh  33965  rezh  33966  dmvlsiga  34126  eulerpartgbij  34370  hgt750lemd  34646  hgt750lem  34649  hgt750lemb  34654  hgt750leme  34656  dnizeq0  36470  cnndvlem1  36532  taupi  37318  poimirlem28  37649  poimirlem31  37652  poimirlem32  37653  asindmre  37704  areacirc  37714  ishlatiN  39355  gcdaddmzz2nni  41989  lcmeprodgcdi  42002  3lexlogpow5ineq1  42049  3lexlogpow2ineq1  42053  rabren3dioph  42810  oaomoencom  43313  inductionexd  44151  lhe4.4ex1a  44325  stoweidlem13  46018  stoweidlem26  46031  stoweidlem34  46039  stoweid  46068  wallispilem2  46071  fourierdlem62  46173  fourierdlem103  46214  fouriersw  46236  salexct3  46347  salgensscntex  46349  smfmullem4  46799  pldofph  46950  31prm  47602  9fppr8  47742  6gbe  47776  8gbe  47778  9gbo  47779  11gbo  47780  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  nnsum4primeseven  47805  tgblthelfgott  47820  tgoldbach  47822  usgrexmpl1lem  48016  usgrexmpl1tri  48020  usgrexmpl2lem  48021  gpg5grlic  48088  gpgprismgr4cycllem2  48090  zlmodzxzldeplem3  48495  zlmodzxzldep  48497  blennnt2  48582  fv2arycl  48641  2arymptfv  48643  line2  48745  line2x  48747  line2y  48748  setc1onsubc  49595