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

Theorem 3pm3.2i 1174
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 975 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
63, 4, 5mpbir2an 918 1  |-  ( ph  /\ 
ps  /\  ch )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  mpbir3an  1178  3jaoi  1291  ftp  6070  hartogslem1  7963  cantnflem3  8106  cantnflem4  8107  cantnflem3OLD  8128  cantnflem4OLD  8129  trcl  8155  ttukeylem7  8891  f13idfv  12070  faclbnd4lem1  12335  hashmap  12455  hashge3el3dif  12486  infcvgaux1i  13627  strleun  14581  strle1  14582  srgbinomlem4  16982  psrass1  17831  psrass23l  17834  psrass23  17836  mplsubrg  17873  mplmon  17896  mplmonmul  17897  mplcoe1  17898  mplbas2  17905  evlslem2  17951  coe1mul2  18081  ply1coeOLD  18109  nn0srg  18254  rge0srg  18255  zfbas  20132  ust0  20457  utop2nei  20488  plypf1  22344  sincos6thpi  22641  1cubr  22901  birthdaylem1  23009  divsqrtsumlem  23037  lgslem2  23300  lgsdir2lem2  23327  lgsdir2lem3  23328  axlowdimlem6  23926  usgraexmpldifpr  24076  2trllemH  24230  2trllemD  24235  2trllemG  24236  wlkntrl  24240  constr2spthlem1  24272  usgra2wlkspthlem2  24296  constr3lem2  24322  constr3trllem2  24327  ex-dvds  24846  sspid  25314  lnocoi  25348  nmlno0lem  25384  nmblolbii  25390  blocnilem  25395  phpar  25415  ip0i  25416  ip2i  25419  ipdirilem  25420  ipasslem10  25430  ip2dii  25435  siilem1  25442  siilem2  25443  hhsst  25858  hhsssh2  25862  fh1i  26215  fh2i  26216  cm2ji  26219  pjoi0i  26312  elunop2  26608  mdslle1i  26912  mdslle2i  26913  mdslj1i  26914  mdslj2i  26915  mdslmd1lem1  26920  mdslmd2i  26925  reofld  27493  xrge0slmod  27497  xrge0iifmhm  27557  cnzh  27587  rezh  27588  dmvlsiga  27769  ddemeas  27848  eulerpartgbij  27951  ballotlem2  28067  quad3  28499  4bc2eq6  28587  asindmre  29679  areacirc  29689  rabren3dioph  30353  lhe4.4ex1a  30834  lptioo2cn  31187  iblsplit  31284  itgsbtaddcnst  31300  stoweidlem13  31313  stoweidlem26  31326  stoweidlem34  31334  stoweid  31363  wallispilem2  31366  dirkerper  31396  dirkercncflem1  31403  dirkercncflem4  31406  fourierdlem62  31469  fourierdlem103  31510  sqwvfoura  31529  sqwvfourb  31530  fouriersw  31532  usgra2pthspth  31820  usgra2pthlem1  31822  zlmodzxzldeplem3  32184  zlmodzxzldep  32186  ishlatiN  34152  taupi  36769
  Copyright terms: Public domain W3C validator