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

Syntax hints:   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  mpbir3an  1343  3jaoi  1429  ftp  7008  hartogslem1  9206  cantnflem3  9354  cantnflem4  9355  trcl  9392  ttukeylem7  10177  f13idfv  13623  faclbnd4lem1  13910  4bc2eq6  13946  hashge3el3dif  14103  funcnvs3  14530  wrdl3s3  14580  infcvgaux1i  15472  halfleoddlt  15974  strleun  16761  strle1  16762  slotstnscsi  16969  slotsdnscsi  16998  slotsbhcdif  17019  slotsbhcdifOLD  17020  setc2obas  17700  estrres  17747  srgbinomlem4  19669  cnfldfun  20497  xrsnsgrp  20521  psrass1  21059  psrass23l  21062  psrass23  21064  mplsubrg  21096  mplmon  21121  mplmonmul  21122  mplcoe1  21123  mplbas2  21128  evlslem2  21174  coe1mul2  21325  zfbas  22930  ust0  23254  utop2nei  23285  isclmi0  24142  iscvsi  24173  plypf1  25253  1cubr  25872  birthdaylem1  25981  divsqrtsumlem  26009  lgslem2  26326  lgsdir2lem2  26354  lgsdir2lem3  26355  addsqn2reu  26469  addsqrexnreu  26470  addsqnreup  26471  axlowdimlem6  27193  usgrexmpldifpr  27503  0grsubgr  27523  upgrewlkle2  27851  usgr2wlkspthlem2  28002  usgr2pthlem  28007  elwspths2spth  28208  wlk2v2e  28397  ntrl2v2e  28398  konigsberglem4  28495  konigsberglem5  28496  ex-dvds  28696  sspid  28963  lnocoi  28995  nmlno0lem  29031  nmblolbii  29037  blocnilem  29042  phpar  29062  ip0i  29063  ip2i  29066  ipdirilem  29067  ipasslem10  29077  ip2dii  29082  siilem1  29089  siilem2  29090  hhssabloilem  29499  hhsst  29504  hhsssh2  29508  fh1i  29859  fh2i  29860  cm2ji  29863  pjoi0i  29956  elunop2  30251  mdslle1i  30555  mdslle2i  30556  mdslj1i  30557  mdslj2i  30558  mdslmd1lem1  30563  mdslmd2i  30568  dp2lt  31036  dpadd3  31063  threehalves  31066  cyc3evpm  31294  xrge0slmod  31425  xrge0iifmhm  31766  cnzh  31795  rezh  31796  dmvlsiga  31972  eulerpartgbij  32214  hgt750lemd  32503  hgt750lem  32506  hgt750lemb  32511  hgt750leme  32513  xpord3ind  33702  on2recsov  33729  nolt02o  33800  nogt01o  33801  noinds  34004  norecov  34006  norec2ov  34016  dnizeq0  34557  cnndvlem1  34619  taupi  35397  poimirlem28  35711  poimirlem31  35714  poimirlem32  35715  asindmre  35766  areacirc  35776  ishlatiN  37275  gcdaddmzz2nni  39910  lcmeprodgcdi  39922  3lexlogpow5ineq1  39969  3lexlogpow2ineq1  39973  rabren3dioph  40525  inductionexd  41627  lhe4.4ex1a  41809  stoweidlem13  43417  stoweidlem26  43430  stoweidlem34  43438  stoweid  43467  wallispilem2  43470  fourierdlem62  43572  fourierdlem103  43613  fouriersw  43635  salexct3  43744  salgensscntex  43746  smfmullem4  44188  pldofph  44300  31prm  44910  9fppr8  45050  6gbe  45084  8gbe  45086  9gbo  45087  11gbo  45088  nnsum4primesodd  45109  nnsum4primesoddALTV  45110  nnsum4primeseven  45113  tgblthelfgott  45128  tgoldbach  45130  zlmodzxzldeplem3  45704  zlmodzxzldep  45706  blennnt2  45796  fv2arycl  45855  2arymptfv  45857  line2  45959  line2x  45961  line2y  45962