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

Theorem mpbiran 909
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 506 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 252 1  |-  ( ph  <->  ch )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
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
This theorem is referenced by:  mpbir2an  911  pm5.63  915  ddif  3483  dfun2  3580  dfin2  3581  0pss  3711  pssv  3713  disj4  3722  zfpair  4524  opabn0  4614  relop  4985  ssrnres  5271  funopab  5446  funcnv2  5472  fnres  5522  dffv2  5759  fnniniseg2OLD  5822  rexsuppOLD  5823  suppssOLD  5831  suppssrOLD  5832  idref  5953  rnoprab  6168  suppssr  6715  brwitnlem  6939  omeu  7016  elixp  7262  1sdom  7507  dfsup2  7684  dfsup2OLD  7685  wemapso2OLD  7758  wemapso2lem  7759  card2inf  7762  harndom  7771  dford2  7818  cantnfp1lem3  7880  cantnfp1  7881  cantnflem1  7889  cantnfleOLD  7901  cantnfp1lem2OLD  7905  cantnfp1lem3OLD  7906  cantnfp1OLD  7907  cantnflem1aOLD  7908  cantnflem1cOLD  7910  cantnflem1OLD  7912  tz9.12lem3  7988  dfac4  8284  dfac12a  8309  cflem  8407  cfsmolem  8431  dffin7-2  8559  dfacfin7  8560  brdom3  8687  iunfo  8695  gch3  8835  lbfzo0  11578  gcdcllem3  13689  1nprm  13760  cygctb  16359  rrgsuppOLD  17340  opsrtoslem2  17541  expmhm  17855  expghm  17898  expghmOLD  17899  basdif0  18533  txdis1cn  19183  trfil2  19435  txflf  19554  clsnsg  19655  tgpconcomp  19658  perfdvf  21353  wilthlem3  22383  mptelee  23092  blocnilem  24155  h1de2i  24907  nmop0  25341  nmfn0  25342  lnopconi  25389  lnfnconi  25410  stcltr2i  25630  funcnvmptOLD  25937  funcnvmpt  25938  1stpreima  25952  2ndpreima  25953  suppss3  25978  dftr6  27511  dfpo2  27516  br6  27518  dford5reg  27546  txpss3v  27860  brsset  27871  dfon3  27874  brtxpsd  27876  brtxpsd2  27877  dffun10  27896  elfuns  27897  funpartlem  27924  fullfunfv  27929  dfrdg4  27932  dfint3  27934  brub  27936  hfext  28172  neibastop2lem  28534  compel  29647  dfdfat2  29990  mat1dimelbas  30790
  Copyright terms: Public domain W3C validator