MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbiran Structured version   Unicode version

Theorem mpbiran 927
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)
Hypotheses
Ref Expression
mpbiran.1  |-  ps
mpbiran.2  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
mpbiran  |-  ( ph  <->  ch )

Proof of Theorem mpbiran
StepHypRef Expression
1 mpbiran.2 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
2 mpbiran.1 . . 3  |-  ps
32biantrur 509 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 256 1  |-  ( ph  <->  ch )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  mpbir2an  929  pm5.63  933  equsexALT  2093  ddif  3598  dfun2  3709  dfin2  3710  0pss  3831  pssv  3833  disj4  3842  zfpair  4656  opabn0  4749  relop  5002  ssrnres  5292  funopab  5632  funcnv2  5658  fnres  5708  dffv2  5952  idref  6159  rnoprab  6391  suppssr  6955  brwitnlem  7215  omeu  7292  elixp  7535  1sdom  7779  dfsup2  7962  wemapso2lem  8071  card2inf  8074  harndom  8083  dford2  8129  cantnfp1lem3  8188  cantnfp1  8189  cantnflem1  8197  tz9.12lem3  8263  dfac4  8555  dfac12a  8580  cflem  8678  cfsmolem  8702  dffin7-2  8830  dfacfin7  8831  brdom3  8958  iunfo  8966  gch3  9103  lbfzo0  11957  gcdcllem3  14468  1nprm  14622  cygctb  17519  opsrtoslem2  18701  expmhm  19028  expghm  19059  mat1dimelbas  19488  basdif0  19960  txdis1cn  20642  trfil2  20894  txflf  21013  clsnsg  21116  tgpconcomp  21119  perfdvf  22850  wilthlem3  23987  mptelee  24917  blocnilem  26437  h1de2i  27198  nmop0  27631  nmfn0  27632  lnopconi  27679  lnfnconi  27700  stcltr2i  27920  funcnvmptOLD  28266  funcnvmpt  28267  1stpreima  28283  2ndpreima  28284  suppss3  28312  elmrsubrn  30160  dftr6  30391  dfpo2  30396  br6  30398  dford5reg  30429  txpss3v  30644  brsset  30655  dfon3  30658  brtxpsd  30660  brtxpsd2  30661  dffun10  30680  elfuns  30681  funpartlem  30708  fullfunfv  30713  dfrdg4  30717  dfint3  30718  brub  30720  hfext  30949  neibastop2lem  31015  bj-equsexv  31305  bj-equsexvv  31306  finxp0  31741  finxp1o  31742  compel  36693  dfdfat2  38389
  Copyright terms: Public domain W3C validator