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 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
6	3, 4, 5	mpbir2an 711	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  1342  3jaoi  1430  ftp  7177  on2recsov  8706  hartogslem1  9582  cantnflem3  9731  cantnflem4  9732  trcl  9768  ttukeylem7  10555  f13idfv  14041  faclbnd4lem1  14332  4bc2eq6  14368  hashge3el3dif  14526  hash3tpb  14534  funcnvs3  14953  wrdl3s3  15001  infcvgaux1i  15893  halfleoddlt  16399  strleun  17194  strle1  17195  slotstnscsi  17404  slotsdnscsi  17436  slotsdifunifndx  17445  slotsbhcdif  17459  slotsbhcdifOLD  17460  setc2obas  18139  estrres  18184  srgbinomlem4  20226  cnfldfunALT  21379  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  xrsnsgrp  21420  psrass1  21984  psrass23l  21987  psrass23  21989  mplsubrg  22025  mplmon  22053  mplmonmul  22054  mplcoe1  22055  mplbas2  22060  evlslem2  22103  coe1mul2  22272  zfbas  23904  ust0  24228  utop2nei  24259  isclmi0  25131  iscvsi  25162  plypf1  26251  1cubr  26885  birthdaylem1  26994  divsqrtsumlem  27023  lgslem2  27342  lgsdir2lem2  27370  lgsdir2lem3  27371  addsqn2reu  27485  addsqrexnreu  27486  addsqnreup  27487  nolt02o  27740  nogt01o  27741  noinds  27978  norecov  27980  norec2ov  27990  nohalf  28407  axlowdimlem6  28962  usgrexmpldifpr  29275  0grsubgr  29295  upgrewlkle2  29624  usgr2wlkspthlem2  29778  usgr2pthlem  29783  elwspths2spth  29987  wlk2v2e  30176  ntrl2v2e  30177  konigsberglem4  30274  konigsberglem5  30275  ex-dvds  30475  sspid  30744  lnocoi  30776  nmlno0lem  30812  nmblolbii  30818  blocnilem  30823  phpar  30843  ip0i  30844  ip2i  30847  ipdirilem  30848  ipasslem10  30858  ip2dii  30863  siilem1  30870  siilem2  30871  hhssabloilem  31280  hhsst  31285  hhsssh2  31289  fh1i  31640  fh2i  31641  cm2ji  31644  pjoi0i  31737  elunop2  32032  mdslle1i  32336  mdslle2i  32337  mdslj1i  32338  mdslj2i  32339  mdslmd1lem1  32344  mdslmd2i  32349  dp2lt  32867  dpadd3  32894  threehalves  32897  cyc3evpm  33170  xrge0slmod  33376  zringfrac  33582  xrge0iifmhm  33938  cnzh  33969  rezh  33970  dmvlsiga  34130  eulerpartgbij  34374  hgt750lemd  34663  hgt750lem  34666  hgt750lemb  34671  hgt750leme  34673  dnizeq0  36476  cnndvlem1  36538  taupi  37324  poimirlem28  37655  poimirlem31  37658  poimirlem32  37659  asindmre  37710  areacirc  37720  ishlatiN  39356  gcdaddmzz2nni  41995  lcmeprodgcdi  42008  3lexlogpow5ineq1  42055  3lexlogpow2ineq1  42059  rabren3dioph  42826  oaomoencom  43330  inductionexd  44168  lhe4.4ex1a  44348  stoweidlem13  46028  stoweidlem26  46041  stoweidlem34  46049  stoweid  46078  wallispilem2  46081  fourierdlem62  46183  fourierdlem103  46224  fouriersw  46246  salexct3  46357  salgensscntex  46359  smfmullem4  46809  pldofph  46957  31prm  47584  9fppr8  47724  6gbe  47758  8gbe  47760  9gbo  47761  11gbo  47762  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primeseven  47787  tgblthelfgott  47802  tgoldbach  47804  usgrexmpl1lem  47980  usgrexmpl1tri  47984  usgrexmpl2lem  47985  gpg5grlic  48047  zlmodzxzldeplem3  48419  zlmodzxzldep  48421  blennnt2  48510  fv2arycl  48569  2arymptfv  48571  line2  48673  line2x  48675  line2y  48676