MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3pm3.2i Structured version   Unicode version

Theorem 3pm3.2i 1166
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
StepHypRef Expression
1 3pm3.2i.1 . . 3  |-  ph
2 3pm3.2i.2 . . 3  |-  ps
31, 2pm3.2i 455 . 2  |-  ( ph  /\ 
ps )
4 3pm3.2i.3 . 2  |-  ch
5 df-3an 967 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
63, 4, 5mpbir2an 911 1  |-  ( ph  /\ 
ps  /\  ch )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  mpbir3an  1170  3jaoi  1281  ftp  5896  hartogslem1  7759  cantnflem3  7902  cantnflem4  7903  cantnflem3OLD  7924  cantnflem4OLD  7925  trcl  7951  ttukeylem7  8687  faclbnd4lem1  12072  hashge3el3dif  12190  hashmap  12200  infcvgaux1i  13322  strleun  14271  strle1  14272  srgbinomlem4  16644  psrass1  17481  psrass23  17485  mplsubrg  17522  mplmon  17545  mplmonmul  17546  mplcoe1  17547  mplbas2  17554  evlslem2  17600  coe1mul2  17726  ply1coeOLD  17750  nn0srg  17884  rge0srg  17885  zfbas  19472  ust0  19797  utop2nei  19828  plypf1  21683  sincos6thpi  21980  1cubr  22240  birthdaylem1  22348  divsqrsumlem  22376  lgslem2  22639  lgsdir2lem2  22666  lgsdir2lem3  22667  axlowdimlem6  23196  usgraexmpldifpr  23321  2trllemH  23454  2trllemD  23459  2trllemG  23460  wlkntrl  23464  constr2spthlem1  23496  constr3lem2  23535  constr3trllem2  23540  ex-dvds  23658  sspid  24126  lnocoi  24160  nmlno0lem  24196  nmblolbii  24202  blocnilem  24207  phpar  24227  ip0i  24228  ip2i  24231  ipdirilem  24232  ipasslem10  24242  ip2dii  24247  siilem1  24254  siilem2  24255  hhsst  24670  hhsssh2  24674  fh1i  25027  fh2i  25028  cm2ji  25031  pjoi0i  25124  elunop2  25420  mdslle1i  25724  mdslle2i  25725  mdslj1i  25726  mdslj2i  25727  mdslmd1lem1  25732  mdslmd2i  25737  reofld  26311  xrge0slmod  26315  xrge0iifmhm  26372  cnzh  26402  rezh  26403  dmvlsiga  26575  ddemeas  26655  eulerpartgbij  26758  ballotlem2  26874  quad3  27306  4bc2eq6  27394  asindmre  28482  areacirc  28492  rabren3dioph  29157  lhe4.4ex1a  29606  stoweidlem13  29811  stoweidlem26  29824  stoweidlem34  29832  stoweid  29861  wallispilem2  29864  f13idfv  30151  usgra2pthspth  30298  usgra2wlkspthlem2  30300  usgra2pthlem1  30303  psrass23l  30827  zlmodzxzldeplem3  31047  zlmodzxzldep  31049  ishlatiN  33003  taupi  35620
  Copyright terms: Public domain W3C validator