Theorem 3pm3.2i 1336

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

Syntax hints:   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  mpbir3an  1338  3jaoi  1424  ftp  6915  hartogslem1  9044  cantnflem3  9192  cantnflem4  9193  trcl  9208  ttukeylem7  9980  f13idfv  13422  faclbnd4lem1  13708  4bc2eq6  13744  hashge3el3dif  13901  funcnvs3  14328  wrdl3s3  14378  infcvgaux1i  15265  halfleoddlt  15768  strleun  16654  strle1  16655  slotsbhcdif  16756  estrres  17460  srgbinomlem4  19366  cnfldfun  20183  xrsnsgrp  20207  psrass1  20738  psrass23l  20741  psrass23  20743  mplsubrg  20775  mplmon  20800  mplmonmul  20801  mplcoe1  20802  mplbas2  20807  evlslem2  20847  coe1mul2  20998  zfbas  22601  ust0  22925  utop2nei  22956  isclmi0  23804  iscvsi  23835  plypf1  24913  1cubr  25532  birthdaylem1  25641  divsqrtsumlem  25669  lgslem2  25986  lgsdir2lem2  26014  lgsdir2lem3  26015  addsqn2reu  26129  addsqrexnreu  26130  addsqnreup  26131  axlowdimlem6  26845  usgrexmpldifpr  27152  0grsubgr  27172  upgrewlkle2  27500  usgr2wlkspthlem2  27651  usgr2pthlem  27656  elwspths2spth  27857  wlk2v2e  28046  ntrl2v2e  28047  konigsberglem4  28144  konigsberglem5  28145  ex-dvds  28345  sspid  28612  lnocoi  28644  nmlno0lem  28680  nmblolbii  28686  blocnilem  28691  phpar  28711  ip0i  28712  ip2i  28715  ipdirilem  28716  ipasslem10  28726  ip2dii  28731  siilem1  28738  siilem2  28739  hhssabloilem  29148  hhsst  29153  hhsssh2  29157  fh1i  29508  fh2i  29509  cm2ji  29512  pjoi0i  29605  elunop2  29900  mdslle1i  30204  mdslle2i  30205  mdslj1i  30206  mdslj2i  30207  mdslmd1lem1  30212  mdslmd2i  30217  dp2lt  30687  dpadd3  30714  threehalves  30717  cyc3evpm  30947  xrge0slmod  31073  xrge0iifmhm  31414  cnzh  31443  rezh  31444  dmvlsiga  31620  eulerpartgbij  31862  hgt750lemd  32151  hgt750lem  32154  hgt750lemb  32159  hgt750leme  32161  xpord3ind  33359  on2recsov  33416  nolt02o  33487  nogt01o  33488  noinds  33676  norecov  33678  norec2ov  33688  dnizeq0  34230  cnndvlem1  34292  taupi  35043  poimirlem28  35391  poimirlem31  35394  poimirlem32  35395  asindmre  35446  areacirc  35456  ishlatiN  36957  gcdaddmzz2nni  39588  lcmeprodgcdi  39600  3lexlogpow5ineq1  39647  3lexlogpow2ineq1  39651  rabren3dioph  40157  inductionexd  41259  lhe4.4ex1a  41434  stoweidlem13  43049  stoweidlem26  43062  stoweidlem34  43070  stoweid  43099  wallispilem2  43102  fourierdlem62  43204  fourierdlem103  43245  fouriersw  43267  salexct3  43376  salgensscntex  43378  smfmullem4  43820  pldofph  43932  31prm  44510  9fppr8  44650  6gbe  44684  8gbe  44686  9gbo  44687  11gbo  44688  nnsum4primesodd  44709  nnsum4primesoddALTV  44710  nnsum4primeseven  44713  tgblthelfgott  44728  tgoldbach  44730  zlmodzxzldeplem3  45304  zlmodzxzldep  45306  blennnt2  45396  fv2arycl  45455  2arymptfv  45457  line2  45559  line2x  45561  line2y  45562