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  7153  on2recsov  8661  hartogslem1  9520  cantnflem3  9676  cantnflem4  9677  trcl  9713  ttukeylem7  10574  f13idfv  14123  faclbnd4lem1  14417  4bc2eq6  14453  hashge3el3dif  14612  hash3tpb  14620  funcnvs3  15045  wrdl3s3  15095  infcvgaux1i  16006  halfleoddlt  16512  strleun  17315  strle1  17316  slotstnscsi  17511  slotsdnscsi  17543  slotsdifunifndx  17552  slotsbhcdif  17566  setc2obas  18249  estrres  18293  srgbinomlem4  20435  cnfldfunALT  21673  xrsnsgrp  21694  psrass1  22251  psrass23l  22254  psrass23  22256  mplsubrg  22292  mplmon  22324  mplmonmul  22325  mplcoe1  22326  mplbas2  22331  evlslem2  22368  coe1mul2  22568  zfbas  24195  ust0  24519  utop2nei  24549  isclmi0  25399  iscvsi  25430  plypf1  26511  1cubr  27152  birthdaylem1  27261  divsqrtsumlem  27289  lgslem2  27607  lgsdir2lem2  27635  lgsdir2lem3  27636  addsqn2reu  27750  addsqrexnreu  27751  addsqnreup  27752  nolt02o  28034  nogt01o  28035  noinds  28313  norecov  28315  norec2ov  28325  bdayfinbndlem1  28835  axlowdimlem6  29507  usgrexmpldifpr  29821  0grsubgr  29841  upgrewlkle2  30169  usgr2wlkspthlem2  30326  usgr2pthlem  30331  elwspths2spth  30541  wlk2v2e  30740  ntrl2v2e  30741  konigsberglem4  30838  konigsberglem5  30839  ex-dvds  31039  sspid  31309  lnocoi  31341  nmlno0lem  31377  nmblolbii  31383  blocnilem  31388  phpar  31408  ip0i  31409  ip2i  31412  ipdirilem  31413  ipasslem10  31423  ip2dii  31428  siilem1  31435  siilem2  31436  hhssabloilem  31845  hhsst  31850  hhsssh2  31854  fh1i  32205  fh2i  32206  cm2ji  32209  pjoi0i  32302  elunop2  32597  mdslle1i  32901  mdslle2i  32902  mdslj1i  32903  mdslj2i  32904  mdslmd1lem1  32909  mdslmd2i  32914  dp2lt  33433  dpadd3  33460  threehalves  33463  cyc3evpm  33693  xrge0slmod  33891  zringfrac  34068  psrmonmul  34164  cos9thpiminplylem5  34400  xrge0iifmhm  34553  cnzh  34582  rezh  34583  dmvlsiga  34743  eulerpartgbij  34987  hgt750lemd  35260  hgt750lem  35263  hgt750lemb  35268  hgt750leme  35270  tz9.1regs  35775  dnizeq0  37311  cnndvlem1  37373  taupi  38212  poimirlem28  38534  poimirlem31  38537  poimirlem32  38538  asindmre  38589  areacirc  38599  ishlatiN  40380  gcdaddmzz2nni  43012  lcmeprodgcdi  43025  3lexlogpow5ineq1  43072  3lexlogpow2ineq1  43076  rabren3dioph  43775  oaomoencom  44277  inductionexd  45114  lhe4.4ex1a  45272  stoweidlem13  46967  stoweidlem26  46980  stoweidlem34  46988  stoweid  47017  wallispilem2  47020  fourierdlem62  47122  fourierdlem103  47163  fouriersw  47185  salexct3  47296  salgensscntex  47298  smfmullem4  47748  pldofph  47959  31prm  48626  9fppr8  48779  6gbe  48813  8gbe  48815  9gbo  48816  11gbo  48817  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  nnsum4primeseven  48842  tgblthelfgott  48857  tgoldbach  48859  usgrexmpl1lem  49063  usgrexmpl1tri  49067  usgrexmpl2lem  49068  gpg5grlim  49135  gpg5grlic  49136  gpgprismgr4cycllem2  49138  zlmodzxzldeplem3  49558  zlmodzxzldep  49560  blennnt2  49645  fv2arycl  49704  2arymptfv  49706  line2  49808  line2x  49810  line2y  49811  setc1onsubc  50654  crosspdotsumlem  50908