Theorem mpbiran 953

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

Step	Hyp	Ref	Expression
1		mpbiran.2	. 2 |- ( ph <-> ( ps /\ ch ) )
2		mpbiran.1	. . 3 |- ps
3	2	biantrur 527	. 2 |- ( ch <-> ( ps /\ ch ) )
4	1, 3	bitr4i 267	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  mpbir2an  955  pm5.63  959  equsexvw  1932  equsexv  2109  equsexALT  2293  ddif  3742  dfun2  3859  dfin2  3860  0pss  4013  pssv  4016  disj4  4025  pwpwab  4614  zfpair  4904  opabn0  5006  relop  5272  ssrnres  5572  funopab  5923  funcnv2  5957  fnres  6007  dffv2  6271  idref  6499  rnoprab  6743  suppssr  7326  brwitnlem  7587  omeu  7665  elixp  7915  1sdom  8163  dfsup2  8350  wemapso2lem  8457  card2inf  8460  harndom  8469  dford2  8517  cantnfp1lem3  8577  cantnfp1  8578  cantnflem1  8586  tz9.12lem3  8652  dfac4  8945  dfac12a  8970  cflem  9068  cfsmolem  9092  dffin7-2  9220  dfacfin7  9221  brdom3  9350  iunfo  9361  gch3  9498  lbfzo0  12507  gcdcllem3  15223  1nprm  15392  cygctb  18293  opsrtoslem2  19485  expmhm  19815  expghm  19844  mat1dimelbas  20277  basdif0  20757  txdis1cn  21438  trfil2  21691  txflf  21810  clsnsg  21913  tgpconncomp  21916  perfdvf  23667  wilthlem3  24796  mptelee  25775  rgrprcx  26488  blocnilem  27659  h1de2i  28412  nmop0  28845  nmfn0  28846  lnopconi  28893  lnfnconi  28914  stcltr2i  29134  funcnvmptOLD  29467  funcnvmpt  29468  1stpreima  29484  2ndpreima  29485  suppss3  29502  elmrsubrn  31417  dftr6  31640  dfpo2  31645  br6  31647  dford5reg  31687  txpss3v  31985  brsset  31996  dfon3  31999  brtxpsd  32001  brtxpsd2  32002  dffun10  32021  elfuns  32022  funpartlem  32049  fullfunfv  32054  dfrdg4  32058  dfint3  32059  brub  32061  hfext  32290  neibastop2lem  32355  bj-equsexval  32638  finxp0  33228  finxp1o  33229  brvdif  34025  xrnss3v  34135  ntrneiel2  38384  ntrneik4w  38398  compel  38641  dfdfat2  41211