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  7095  on2recsov  8593  hartogslem1  9453  cantnflem3  9606  cantnflem4  9607  trcl  9643  ttukeylem7  10428  f13idfv  13925  faclbnd4lem1  14218  4bc2eq6  14254  hashge3el3dif  14412  hash3tpb  14420  funcnvs3  14839  wrdl3s3  14887  infcvgaux1i  15782  halfleoddlt  16291  strleun  17086  strle1  17087  slotstnscsi  17282  slotsdnscsi  17314  slotsdifunifndx  17323  slotsbhcdif  17337  setc2obas  18019  estrres  18063  srgbinomlem4  20132  cnfldfunALT  21294  cnfldfunALTOLD  21307  xrsnsgrp  21332  psrass1  21889  psrass23l  21892  psrass23  21894  mplsubrg  21930  mplmon  21958  mplmonmul  21959  mplcoe1  21960  mplbas2  21965  evlslem2  22002  coe1mul2  22171  zfbas  23799  ust0  24123  utop2nei  24154  isclmi0  25014  iscvsi  25045  plypf1  26133  1cubr  26768  birthdaylem1  26877  divsqrtsumlem  26906  lgslem2  27225  lgsdir2lem2  27253  lgsdir2lem3  27254  addsqn2reu  27368  addsqrexnreu  27369  addsqnreup  27370  nolt02o  27623  nogt01o  27624  noinds  27875  norecov  27877  norec2ov  27887  axlowdimlem6  28910  usgrexmpldifpr  29221  0grsubgr  29241  upgrewlkle2  29570  usgr2wlkspthlem2  29721  usgr2pthlem  29726  elwspths2spth  29930  wlk2v2e  30119  ntrl2v2e  30120  konigsberglem4  30217  konigsberglem5  30218  ex-dvds  30418  sspid  30687  lnocoi  30719  nmlno0lem  30755  nmblolbii  30761  blocnilem  30766  phpar  30786  ip0i  30787  ip2i  30790  ipdirilem  30791  ipasslem10  30801  ip2dii  30806  siilem1  30813  siilem2  30814  hhssabloilem  31223  hhsst  31228  hhsssh2  31232  fh1i  31583  fh2i  31584  cm2ji  31587  pjoi0i  31680  elunop2  31975  mdslle1i  32279  mdslle2i  32280  mdslj1i  32281  mdslj2i  32282  mdslmd1lem1  32287  mdslmd2i  32292  dp2lt  32838  dpadd3  32865  threehalves  32868  cyc3evpm  33105  xrge0slmod  33295  zringfrac  33501  cos9thpiminplylem5  33752  xrge0iifmhm  33905  cnzh  33934  rezh  33935  dmvlsiga  34095  eulerpartgbij  34339  hgt750lemd  34615  hgt750lem  34618  hgt750lemb  34623  hgt750leme  34625  tz9.1regs  35066  dnizeq0  36448  cnndvlem1  36510  taupi  37296  poimirlem28  37627  poimirlem31  37630  poimirlem32  37631  asindmre  37682  areacirc  37692  ishlatiN  39333  gcdaddmzz2nni  41967  lcmeprodgcdi  41980  3lexlogpow5ineq1  42027  3lexlogpow2ineq1  42031  rabren3dioph  42788  oaomoencom  43290  inductionexd  44128  lhe4.4ex1a  44302  stoweidlem13  45995  stoweidlem26  46008  stoweidlem34  46016  stoweid  46045  wallispilem2  46048  fourierdlem62  46150  fourierdlem103  46191  fouriersw  46213  salexct3  46324  salgensscntex  46326  smfmullem4  46776  pldofph  46930  31prm  47582  9fppr8  47722  6gbe  47756  8gbe  47758  9gbo  47759  11gbo  47760  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  nnsum4primeseven  47785  tgblthelfgott  47800  tgoldbach  47802  usgrexmpl1lem  48006  usgrexmpl1tri  48010  usgrexmpl2lem  48011  gpg5grlim  48078  gpg5grlic  48079  gpgprismgr4cycllem2  48081  zlmodzxzldeplem3  48488  zlmodzxzldep  48490  blennnt2  48575  fv2arycl  48634  2arymptfv  48636  line2  48738  line2x  48740  line2y  48741  setc1onsubc  49588