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

Theorem 3pm3.2i 1208
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 462 . 2  |-  ( ph  /\ 
ps )
4 3pm3.2i.3 . 2  |-  ch
5 df-3an 1009 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
63, 4, 5mpbir2an 934 1  |-  ( ph  /\ 
ps  /\  ch )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  mpbir3an  1212  3jaoi  1357  ftp  6091  hartogslem1  8075  cantnflem3  8214  cantnflem4  8215  trcl  8230  ttukeylem7  8963  f13idfv  12250  faclbnd4lem1  12516  4bc2eq6  12552  hashmap  12648  hashge3el3dif  12683  funcnvs3  13068  infcvgaux1i  13992  fprodge0  14124  fprodge1  14126  strleun  15298  strle1  15299  slotsbhcdif  15396  estrres  16102  srgbinomlem4  17854  psrass1  18706  psrass23l  18709  psrass23  18711  mplsubrg  18741  mplmon  18764  mplmonmul  18765  mplcoe1  18766  mplbas2  18771  evlslem2  18812  coe1mul2  18939  ply1coeOLD  18967  xrsnsgrp  19081  zfbas  20989  ust0  21312  utop2nei  21343  plypf1  23245  logblog  23808  1cubr  23847  birthdaylem1  23956  divsqrtsumlem  23984  lgslem2  24304  lgsdir2lem2  24331  lgsdir2lem3  24332  axlowdimlem6  25056  usgraexmpldifpr  25206  2trllemH  25361  2trllemD  25366  2trllemG  25367  wlkntrl  25371  constr2spthlem1  25403  usgra2wlkspthlem2  25427  constr3lem2  25453  constr3trllem2  25458  ex-dvds  25977  sspid  26445  lnocoi  26479  nmlno0lem  26515  nmblolbii  26521  blocnilem  26526  phpar  26546  ip0i  26547  ip2i  26550  ipdirilem  26551  ipasslem10  26561  ip2dii  26566  siilem1  26573  siilem2  26574  hhsst  26998  hhsssh2  27002  fh1i  27355  fh2i  27356  cm2ji  27359  pjoi0i  27452  elunop2  27747  mdslle1i  28051  mdslle2i  28052  mdslj1i  28053  mdslj2i  28054  mdslmd1lem1  28059  mdslmd2i  28064  xrge0slmod  28681  xrge0iifmhm  28819  cnzh  28848  rezh  28849  dmvlsiga  29025  eulerpartgbij  29278  taupi  31794  poimirlem28  32032  poimirlem31  32035  poimirlem32  32036  asindmre  32091  areacirc  32101  ishlatiN  32992  rabren3dioph  35729  inductionexd  36664  lhe4.4ex1a  36748  stoweidlem13  37985  stoweidlem26  37998  stoweidlem34  38007  stoweid  38037  wallispilem2  38040  fourierdlem62  38144  fourierdlem103  38185  fouriersw  38207  salexct3  38313  salgensscntex  38315  pldofph  38678  6gbe  39017  8gbe  39019  9gboa  39020  11gboa  39021  nnsum4primesodd  39036  nnsum4primesoddALTV  39037  nnsum4primeseven  39040  tgblthelfgott  39053  tgoldbach  39056  funsneqopsn  39169  0grsubgr  39514  upgrewlkle2  39812  usgr2wlkspthlem2  39950  1wlk2v2e  40045  ntrl2v2e  40046  konigsberglem4  40169  konigsberglem5  40170  usgra2pthspth  40173  usgra2pthlem1  40175  zlmodzxzldeplem3  40803  zlmodzxzldep  40805  blennnt2  40908
  Copyright terms: Public domain W3C validator