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  7146  on2recsov  8678  hartogslem1  9554  cantnflem3  9703  cantnflem4  9704  trcl  9740  ttukeylem7  10527  f13idfv  14016  faclbnd4lem1  14309  4bc2eq6  14345  hashge3el3dif  14503  hash3tpb  14511  funcnvs3  14931  wrdl3s3  14979  infcvgaux1i  15871  halfleoddlt  16379  strleun  17174  strle1  17175  slotstnscsi  17372  slotsdnscsi  17404  slotsdifunifndx  17413  slotsbhcdif  17427  setc2obas  18105  estrres  18149  srgbinomlem4  20187  cnfldfunALT  21328  cnfldfunALTOLD  21341  xrsnsgrp  21368  psrass1  21922  psrass23l  21925  psrass23  21927  mplsubrg  21963  mplmon  21991  mplmonmul  21992  mplcoe1  21993  mplbas2  21998  evlslem2  22035  coe1mul2  22204  zfbas  23832  ust0  24156  utop2nei  24187  isclmi0  25047  iscvsi  25078  plypf1  26167  1cubr  26802  birthdaylem1  26911  divsqrtsumlem  26940  lgslem2  27259  lgsdir2lem2  27287  lgsdir2lem3  27288  addsqn2reu  27402  addsqrexnreu  27403  addsqnreup  27404  nolt02o  27657  nogt01o  27658  noinds  27895  norecov  27897  norec2ov  27907  nohalf  28324  axlowdimlem6  28872  usgrexmpldifpr  29183  0grsubgr  29203  upgrewlkle2  29532  usgr2wlkspthlem2  29686  usgr2pthlem  29691  elwspths2spth  29895  wlk2v2e  30084  ntrl2v2e  30085  konigsberglem4  30182  konigsberglem5  30183  ex-dvds  30383  sspid  30652  lnocoi  30684  nmlno0lem  30720  nmblolbii  30726  blocnilem  30731  phpar  30751  ip0i  30752  ip2i  30755  ipdirilem  30756  ipasslem10  30766  ip2dii  30771  siilem1  30778  siilem2  30779  hhssabloilem  31188  hhsst  31193  hhsssh2  31197  fh1i  31548  fh2i  31549  cm2ji  31552  pjoi0i  31645  elunop2  31940  mdslle1i  32244  mdslle2i  32245  mdslj1i  32246  mdslj2i  32247  mdslmd1lem1  32252  mdslmd2i  32257  dp2lt  32805  dpadd3  32832  threehalves  32835  cyc3evpm  33107  xrge0slmod  33309  zringfrac  33515  cos9thpiminplylem5  33766  xrge0iifmhm  33916  cnzh  33945  rezh  33946  dmvlsiga  34106  eulerpartgbij  34350  hgt750lemd  34626  hgt750lem  34629  hgt750lemb  34634  hgt750leme  34636  dnizeq0  36439  cnndvlem1  36501  taupi  37287  poimirlem28  37618  poimirlem31  37621  poimirlem32  37622  asindmre  37673  areacirc  37683  ishlatiN  39319  gcdaddmzz2nni  41953  lcmeprodgcdi  41966  3lexlogpow5ineq1  42013  3lexlogpow2ineq1  42017  rabren3dioph  42785  oaomoencom  43288  inductionexd  44126  lhe4.4ex1a  44301  stoweidlem13  45990  stoweidlem26  46003  stoweidlem34  46011  stoweid  46040  wallispilem2  46043  fourierdlem62  46145  fourierdlem103  46186  fouriersw  46208  salexct3  46319  salgensscntex  46321  smfmullem4  46771  pldofph  46922  31prm  47559  9fppr8  47699  6gbe  47733  8gbe  47735  9gbo  47736  11gbo  47737  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  nnsum4primeseven  47762  tgblthelfgott  47777  tgoldbach  47779  usgrexmpl1lem  47973  usgrexmpl1tri  47977  usgrexmpl2lem  47978  gpg5grlic  48041  gpgprismgr4cycllem2  48043  zlmodzxzldeplem3  48426  zlmodzxzldep  48428  blennnt2  48517  fv2arycl  48576  2arymptfv  48578  line2  48680  line2x  48682  line2y  48683  setc1onsubc  49427