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

Theorem mpbiran 928
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  930  pm5.63  934  equsexvw  1847  equsexv  2065  equsexALT  2130  ddif  3564  dfun2  3677  dfin2  3678  0pss  3801  pssv  3803  disj4  3812  zfpair  4636  opabn0  4731  relop  4984  ssrnres  5274  funopab  5614  funcnv2  5640  fnres  5690  dffv2  5936  idref  6144  rnoprab  6376  suppssr  6943  brwitnlem  7206  omeu  7283  elixp  7526  1sdom  7772  dfsup2  7955  wemapso2lem  8064  card2inf  8067  harndom  8076  dford2  8122  cantnfp1lem3  8182  cantnfp1  8183  cantnflem1  8191  tz9.12lem3  8257  dfac4  8550  dfac12a  8575  cflem  8673  cfsmolem  8697  dffin7-2  8825  dfacfin7  8826  brdom3  8953  iunfo  8961  gch3  9098  lbfzo0  11952  gcdcllem3  14468  1nprm  14622  cygctb  17519  opsrtoslem2  18701  expmhm  19029  expghm  19060  mat1dimelbas  19489  basdif0  19961  txdis1cn  20643  trfil2  20895  txflf  21014  clsnsg  21117  tgpconcomp  21120  perfdvf  22851  wilthlem3  23988  mptelee  24918  blocnilem  26438  h1de2i  27199  nmop0  27632  nmfn0  27633  lnopconi  27680  lnfnconi  27701  stcltr2i  27921  funcnvmptOLD  28263  funcnvmpt  28264  1stpreima  28280  2ndpreima  28281  suppss3  28305  elmrsubrn  30151  dftr6  30383  dfpo2  30388  br6  30390  dford5reg  30421  txpss3v  30638  brsset  30649  dfon3  30652  brtxpsd  30654  brtxpsd2  30655  dffun10  30674  elfuns  30675  funpartlem  30702  fullfunfv  30707  dfrdg4  30711  dfint3  30712  brub  30714  hfext  30943  neibastop2lem  31009  bj-equsexval  31244  finxp0  31776  finxp1o  31777  compel  36785  dfdfat2  38627  rgrprcx  39590
  Copyright terms: Public domain W3C validator