Theorem 3pm3.2i 1358

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

This proof depends on syntax axioms:   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mpbir3an  1360  3jaoiOLD  1455  ftp  7158  on2recsov  8660  hartogslem1  9518  cantnflem3  9674  cantnflem4  9675  trcl  9711  ttukeylem7  10521  f13idfv  14068  faclbnd4lem1  14361  4bc2eq6  14397  hashge3el3dif  14556  hash3tpb  14564  funcnvs3  14989  wrdl3s3  15039  infcvgaux1i  15950  halfleoddlt  16458  strleun  17255  strle1  17256  slotstnscsi  17451  slotsdnscsi  17483  slotsdifunifndx  17492  slotsbhcdif  17506  setc2obas  18189  estrres  18233  srgbinomlem4  20374  cnfldfunALT  21606  xrsnsgrp  21627  psrass1  22184  psrass23l  22187  psrass23  22189  mplsubrg  22225  mplmon  22257  mplmonmul  22258  mplcoe1  22259  mplbas2  22264  evlslem2  22301  coe1mul2  22501  zfbas  24128  ust0  24452  utop2nei  24482  isclmi0  25332  iscvsi  25363  plypf1  26445  1cubr  27087  birthdaylem1  27196  divsqrtsumlem  27224  lgslem2  27542  lgsdir2lem2  27570  lgsdir2lem3  27571  addsqn2reu  27685  addsqrexnreu  27686  addsqnreup  27687  nolt02o  27939  nogt01o  27940  noinds  28218  norecov  28220  norec2ov  28230  bdayfinbndlem1  28740  axlowdimlem6  29412  usgrexmpldifpr  29726  0grsubgr  29746  upgrewlkle2  30074  usgr2wlkspthlem2  30231  usgr2pthlem  30236  elwspths2spth  30446  wlk2v2e  30645  ntrl2v2e  30646  konigsberglem4  30743  konigsberglem5  30744  ex-dvds  30944  sspid  31214  lnocoi  31246  nmlno0lem  31282  nmblolbii  31288  blocnilem  31293  phpar  31313  ip0i  31314  ip2i  31317  ipdirilem  31318  ipasslem10  31328  ip2dii  31333  siilem1  31340  siilem2  31341  hhssabloilem  31750  hhsst  31755  hhsssh2  31759  fh1i  32110  fh2i  32111  cm2ji  32114  pjoi0i  32207  elunop2  32502  mdslle1i  32806  mdslle2i  32807  mdslj1i  32808  mdslj2i  32809  mdslmd1lem1  32814  mdslmd2i  32819  dp2lt  33338  dpadd3  33365  threehalves  33368  cyc3evpm  33598  xrge0slmod  33796  zringfrac  33972  psrmonmul  34068  cos9thpiminplylem5  34304  xrge0iifmhm  34457  cnzh  34486  rezh  34487  dmvlsiga  34647  eulerpartgbij  34891  hgt750lemd  35164  hgt750lem  35167  hgt750lemb  35172  hgt750leme  35174  tz9.1regs  35668  dnizeq0  37180  cnndvlem1  37242  taupi  38083  poimirlem28  38405  poimirlem31  38408  poimirlem32  38409  asindmre  38460  areacirc  38470  ishlatiN  40236  gcdaddmzz2nni  42868  lcmeprodgcdi  42881  3lexlogpow5ineq1  42928  3lexlogpow2ineq1  42932  rabren3dioph  43664  oaomoencom  44166  inductionexd  45003  lhe4.4ex1a  45161  stoweidlem13  46849  stoweidlem26  46862  stoweidlem34  46870  stoweid  46899  wallispilem2  46902  fourierdlem62  47004  fourierdlem103  47045  fouriersw  47067  salexct3  47178  salgensscntex  47180  smfmullem4  47630  pldofph  47841  31prm  48508  9fppr8  48661  6gbe  48695  8gbe  48697  9gbo  48698  11gbo  48699  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  nnsum4primeseven  48724  tgblthelfgott  48739  tgoldbach  48741  usgrexmpl1lem  48945  usgrexmpl1tri  48949  usgrexmpl2lem  48950  gpg5grlim  49017  gpg5grlic  49018  gpgprismgr4cycllem2  49020  zlmodzxzldeplem3  49440  zlmodzxzldep  49442  blennnt2  49527  fv2arycl  49586  2arymptfv  49588  line2  49690  line2x  49692  line2y  49693  setc1onsubc  50536  crosspdotsumlem  50805