Theorem 3pm3.2i 1239

Description: Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)

Hypotheses

Ref	Expression
3pm3.2i.1	|- ph
3pm3.2i.2	|- ps
3pm3.2i.3	|- ch

Assertion

Ref	Expression
3pm3.2i	|- ( ph /\ ps /\ ch )

Proof of Theorem 3pm3.2i

Step	Hyp	Ref	Expression
1		3pm3.2i.1	. . 3 |- ph
2		3pm3.2i.2	. . 3 |- ps
3	1, 2	pm3.2i 471	. 2 |- ( ph /\ ps )
4		3pm3.2i.3	. 2 |- ch
5		df-3an 1039	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
6	3, 4, 5	mpbir2an 955	1 |- ( ph /\ ps /\ ch )

Syntax hints:   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  mpbir3an  1244  3jaoi  1391  funsneqopsn  6417  ftp  6424  hartogslem1  8447  cantnflem3  8588  cantnflem4  8589  trcl  8604  ttukeylem7  9337  f13idfv  12800  faclbnd4lem1  13080  4bc2eq6  13116  hashmap  13222  hashge3el3dif  13268  funcnvs3  13659  wrdl3s3  13705  infcvgaux1i  14589  fprodge0  14724  fprodge1  14726  halfleoddlt  15086  strleun  15972  strle1  15973  slotsbhcdif  16080  estrres  16779  srgbinomlem4  18543  psrass1  19405  psrass23l  19408  psrass23  19410  mplsubrg  19440  mplmon  19463  mplmonmul  19464  mplcoe1  19465  mplbas2  19470  evlslem2  19512  coe1mul2  19639  cnfldfun  19758  xrsnsgrp  19782  zfbas  21700  ust0  22023  utop2nei  22054  isclmi0  22898  iscvsi  22929  plypf1  23968  logblog  24530  1cubr  24569  birthdaylem1  24678  divsqrtsumlem  24706  lgslem2  25023  lgsdir2lem2  25051  lgsdir2lem3  25052  axlowdimlem6  25827  usgrexmpldifpr  26150  0grsubgr  26170  upgrewlkle2  26502  usgr2wlkspthlem2  26654  usgr2pthlem  26659  elwspths2spth  26862  wlk2v2e  27017  ntrl2v2e  27018  konigsberglem4  27117  konigsberglem5  27118  ex-dvds  27313  sspid  27580  lnocoi  27612  nmlno0lem  27648  nmblolbii  27654  blocnilem  27659  phpar  27679  ip0i  27680  ip2i  27683  ipdirilem  27684  ipasslem10  27694  ip2dii  27699  siilem1  27706  siilem2  27707  hhssabloilem  28118  hhsst  28123  hhsssh2  28127  fh1i  28480  fh2i  28481  cm2ji  28484  pjoi0i  28577  elunop2  28872  mdslle1i  29176  mdslle2i  29177  mdslj1i  29178  mdslj2i  29179  mdslmd1lem1  29184  mdslmd2i  29189  dp2lt  29592  dpadd3  29620  threehalves  29623  xrge0slmod  29844  xrge0iifmhm  29985  cnzh  30014  rezh  30015  dmvlsiga  30192  eulerpartgbij  30434  hgt750lemd  30726  hgt750lem  30729  hgt750lemb  30734  hgt750leme  30736  nolt02o  31845  dnizeq0  32465  cnndvlem1  32528  taupi  33169  poimirlem28  33437  poimirlem31  33440  poimirlem32  33441  asindmre  33495  areacirc  33505  ishlatiN  34642  rabren3dioph  37379  inductionexd  38453  lhe4.4ex1a  38528  stoweidlem13  40230  stoweidlem26  40243  stoweidlem34  40251  stoweid  40280  wallispilem2  40283  fourierdlem62  40385  fourierdlem103  40426  fouriersw  40448  salexct3  40560  salgensscntex  40562  smfmullem4  41001  pldofph  41112  31prm  41512  6gbe  41659  8gbe  41661  9gbo  41662  11gbo  41663  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  tgblthelfgott  41703  tgoldbach  41705  tgblthelfgottOLD  41709  tgoldbachOLD  41712  zlmodzxzldeplem3  42291  zlmodzxzldep  42293  blennnt2  42383