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

Theorem 3pm3.2i 1159
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 452 . 2  |-  ( ph  /\ 
ps )
4 3pm3.2i.3 . 2  |-  ch
5 df-3an 960 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
63, 4, 5mpbir2an 904 1  |-  ( ph  /\ 
ps  /\  ch )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  mpbir3an  1163  3jaoi  1274  ftp  5880  hartogslem1  7744  cantnflem3  7887  cantnflem4  7888  cantnflem3OLD  7909  cantnflem4OLD  7910  trcl  7936  ttukeylem7  8672  faclbnd4lem1  12053  hashge3el3dif  12171  hashmap  12181  infcvgaux1i  13302  strleun  14251  strle1  14252  psrass1  17412  psrass23  17416  mplsubrg  17453  mplmon  17476  mplmonmul  17477  mplcoe1  17478  mplbas2  17483  evlslem2  17525  coe1mul2  17621  ply1coe  17643  zfbas  19311  ust0  19636  utop2nei  19667  plypf1  21565  sincos6thpi  21862  1cubr  22122  birthdaylem1  22230  divsqrsumlem  22258  lgslem2  22521  lgsdir2lem2  22548  lgsdir2lem3  22549  axlowdimlem6  23016  usgraexmpldifpr  23141  2trllemH  23274  2trllemD  23279  2trllemG  23280  wlkntrl  23284  constr2spthlem1  23316  constr3lem2  23355  constr3trllem2  23360  ex-dvds  23478  sspid  23946  lnocoi  23980  nmlno0lem  24016  nmblolbii  24022  blocnilem  24027  phpar  24047  ip0i  24048  ip2i  24051  ipdirilem  24052  ipasslem10  24062  ip2dii  24067  siilem1  24074  siilem2  24075  hhsst  24490  hhsssh2  24494  fh1i  24847  fh2i  24848  cm2ji  24851  pjoi0i  24944  elunop2  25240  mdslle1i  25544  mdslle2i  25545  mdslj1i  25546  mdslj2i  25547  mdslmd1lem1  25552  mdslmd2i  25557  nn0srg  26063  rge0srg  26064  reofld  26162  xrge0slmod  26166  xrge0iifmhm  26223  cnzh  26253  rezh  26254  dmvlsiga  26426  ddemeas  26506  eulerpartgbij  26603  ballotlem2  26719  4bc2eq6  27238  asindmre  28323  areacirc  28333  rabren3dioph  28999  areaquad  29437  lhe4.4ex1a  29448  stoweidlem13  29654  stoweidlem26  29667  stoweidlem34  29675  stoweid  29704  wallispilem2  29707  f13idfv  29994  usgra2pthspth  30141  usgra2wlkspthlem2  30143  usgra2pthlem1  30146  ply1coefsupp  30634  zlmodzxzldeplem3  30753  zlmodzxzldep  30755  ishlatiN  32573  taupi  35190
  Copyright terms: Public domain W3C validator