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

Theorem mpbiran 902
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 503 . 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  904  pm5.63  908  ddif  3476  dfun2  3573  dfin2  3574  0pss  3704  pssv  3706  disj4  3715  zfpair  4517  opabn0  4608  relop  4977  ssrnres  5264  funopab  5439  funcnv2  5465  fnres  5515  dffv2  5752  fnniniseg2OLD  5815  rexsuppOLD  5816  suppssOLD  5824  suppssrOLD  5825  idref  5945  rnoprab  6162  suppssr  6709  brwitnlem  6935  omeu  7012  elixp  7258  1sdom  7503  dfsup2  7680  dfsup2OLD  7681  wemapso2OLD  7754  wemapso2lem  7755  card2inf  7758  harndom  7767  dford2  7814  cantnfp1lem3  7876  cantnfp1  7877  cantnflem1  7885  cantnfleOLD  7897  cantnfp1lem2OLD  7901  cantnfp1lem3OLD  7902  cantnfp1OLD  7903  cantnflem1aOLD  7904  cantnflem1cOLD  7906  cantnflem1OLD  7908  tz9.12lem3  7984  dfac4  8280  dfac12a  8305  cflem  8403  cfsmolem  8427  dffin7-2  8555  dfacfin7  8556  brdom3  8683  iunfo  8691  gch3  8830  lbfzo0  11569  gcdcllem3  13679  1nprm  13750  cygctb  16347  rrgsuppOLD  17284  opsrtoslem2  17497  expmhm  17723  expghm  17764  expghmOLD  17765  basdif0  18399  txdis1cn  19049  trfil2  19301  txflf  19420  clsnsg  19521  tgpconcomp  19524  perfdvf  21219  wilthlem3  22292  mptelee  22963  blocnilem  24026  h1de2i  24778  nmop0  25212  nmfn0  25213  lnopconi  25260  lnfnconi  25281  stcltr2i  25501  funcnvmptOLD  25809  funcnvmpt  25810  1stpreima  25824  2ndpreima  25825  suppss3  25850  dftr6  27406  dfpo2  27411  br6  27413  dford5reg  27441  txpss3v  27755  brsset  27766  dfon3  27769  brtxpsd  27771  brtxpsd2  27772  dffun10  27791  elfuns  27792  funpartlem  27819  fullfunfv  27824  dfrdg4  27827  dfint3  27829  brub  27831  hfext  28067  neibastop2lem  28422  compel  29536  dfdfat2  29880
  Copyright terms: Public domain W3C validator