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

Theorem mpbiran 918
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  920  pm5.63  924  ddif  3621  dfun2  3718  dfin2  3719  0pss  3850  pssv  3852  disj4  3861  zfpair  4674  opabn0  4768  relop  5143  ssrnres  5435  funopab  5611  funcnv2  5637  fnres  5687  dffv2  5931  fnniniseg2OLD  5996  rexsuppOLD  5997  suppssOLD  6005  suppssrOLD  6006  idref  6138  rnoprab  6370  suppssr  6933  brwitnlem  7159  omeu  7236  elixp  7478  1sdom  7724  dfsup2  7904  dfsup2OLD  7905  wemapso2OLD  7980  wemapso2lem  7981  card2inf  7984  harndom  7993  dford2  8040  cantnfp1lem3  8102  cantnfp1  8103  cantnflem1  8111  cantnfleOLD  8123  cantnfp1lem2OLD  8127  cantnfp1lem3OLD  8128  cantnfp1OLD  8129  cantnflem1aOLD  8130  cantnflem1cOLD  8132  cantnflem1OLD  8134  tz9.12lem3  8210  dfac4  8506  dfac12a  8531  cflem  8629  cfsmolem  8653  dffin7-2  8781  dfacfin7  8782  brdom3  8909  iunfo  8917  gch3  9057  lbfzo0  11844  gcdcllem3  14133  1nprm  14204  cygctb  16873  rrgsuppOLD  17919  opsrtoslem2  18128  expmhm  18464  expghm  18507  expghmOLD  18508  mat1dimelbas  18951  basdif0  19432  txdis1cn  20114  trfil2  20366  txflf  20485  clsnsg  20586  tgpconcomp  20589  perfdvf  22285  wilthlem3  23322  mptelee  24176  blocnilem  25697  h1de2i  26449  nmop0  26883  nmfn0  26884  lnopconi  26931  lnfnconi  26952  stcltr2i  27172  funcnvmptOLD  27487  funcnvmpt  27488  1stpreima  27502  2ndpreima  27503  suppss3  27528  elmrsubrn  28858  dftr6  29155  dfpo2  29160  br6  29162  dford5reg  29190  txpss3v  29504  brsset  29515  dfon3  29518  brtxpsd  29520  brtxpsd2  29521  dffun10  29540  elfuns  29541  funpartlem  29568  fullfunfv  29573  dfrdg4  29576  dfint3  29578  brub  29580  hfext  29816  neibastop2lem  30154  compel  31301  dfdfat2  32170
  Copyright terms: Public domain W3C validator