Theorem 3pm3.2i 1341

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 712	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  1343  3jaoi  1431  ftp  7104  on2recsov  8597  hartogslem1  9450  cantnflem3  9603  cantnflem4  9604  trcl  9640  ttukeylem7  10428  f13idfv  13953  faclbnd4lem1  14246  4bc2eq6  14282  hashge3el3dif  14440  hash3tpb  14448  funcnvs3  14867  wrdl3s3  14915  infcvgaux1i  15813  halfleoddlt  16322  strleun  17118  strle1  17119  slotstnscsi  17314  slotsdnscsi  17346  slotsdifunifndx  17355  slotsbhcdif  17369  setc2obas  18052  estrres  18096  srgbinomlem4  20201  cnfldfunALT  21359  cnfldfunALTOLD  21372  xrsnsgrp  21397  psrass1  21952  psrass23l  21955  psrass23  21957  mplsubrg  21993  mplmon  22023  mplmonmul  22024  mplcoe1  22025  mplbas2  22030  evlslem2  22067  coe1mul2  22244  zfbas  23871  ust0  24195  utop2nei  24225  isclmi0  25075  iscvsi  25106  plypf1  26187  1cubr  26819  birthdaylem1  26928  divsqrtsumlem  26957  lgslem2  27275  lgsdir2lem2  27303  lgsdir2lem3  27304  addsqn2reu  27418  addsqrexnreu  27419  addsqnreup  27420  nolt02o  27673  nogt01o  27674  noinds  27951  norecov  27953  norec2ov  27963  bdayfinbndlem1  28473  axlowdimlem6  29030  usgrexmpldifpr  29341  0grsubgr  29361  upgrewlkle2  29690  usgr2wlkspthlem2  29841  usgr2pthlem  29846  elwspths2spth  30053  wlk2v2e  30242  ntrl2v2e  30243  konigsberglem4  30340  konigsberglem5  30341  ex-dvds  30541  sspid  30811  lnocoi  30843  nmlno0lem  30879  nmblolbii  30885  blocnilem  30890  phpar  30910  ip0i  30911  ip2i  30914  ipdirilem  30915  ipasslem10  30925  ip2dii  30930  siilem1  30937  siilem2  30938  hhssabloilem  31347  hhsst  31352  hhsssh2  31356  fh1i  31707  fh2i  31708  cm2ji  31711  pjoi0i  31804  elunop2  32099  mdslle1i  32403  mdslle2i  32404  mdslj1i  32405  mdslj2i  32406  mdslmd1lem1  32411  mdslmd2i  32416  dp2lt  32959  dpadd3  32986  threehalves  32989  cyc3evpm  33226  xrge0slmod  33423  zringfrac  33629  psrmonmul  33709  cos9thpiminplylem5  33946  xrge0iifmhm  34099  cnzh  34128  rezh  34129  dmvlsiga  34289  eulerpartgbij  34532  hgt750lemd  34808  hgt750lem  34811  hgt750lemb  34816  hgt750leme  34818  tz9.1regs  35294  dnizeq0  36751  cnndvlem1  36813  taupi  37653  poimirlem28  37983  poimirlem31  37986  poimirlem32  37987  asindmre  38038  areacirc  38048  ishlatiN  39815  gcdaddmzz2nni  42447  lcmeprodgcdi  42460  3lexlogpow5ineq1  42507  3lexlogpow2ineq1  42511  rabren3dioph  43261  oaomoencom  43763  inductionexd  44600  lhe4.4ex1a  44774  stoweidlem13  46459  stoweidlem26  46472  stoweidlem34  46480  stoweid  46509  wallispilem2  46512  fourierdlem62  46614  fourierdlem103  46655  fouriersw  46677  salexct3  46788  salgensscntex  46790  smfmullem4  47240  pldofph  47405  31prm  48072  9fppr8  48225  6gbe  48259  8gbe  48261  9gbo  48262  11gbo  48263  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  nnsum4primeseven  48288  tgblthelfgott  48303  tgoldbach  48305  usgrexmpl1lem  48509  usgrexmpl1tri  48513  usgrexmpl2lem  48514  gpg5grlim  48581  gpg5grlic  48582  gpgprismgr4cycllem2  48584  zlmodzxzldeplem3  48990  zlmodzxzldep  48992  blennnt2  49077  fv2arycl  49136  2arymptfv  49138  line2  49240  line2x  49242  line2y  49243  setc1onsubc  50089