Theorem mpbiran 709

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)

Hypotheses

Ref	Expression
mpbiran.1	⊢ 𝜓
mpbiran.2	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
mpbiran	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem mpbiran

Step	Hyp	Ref	Expression
1		mpbiran.2	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		mpbiran.1	. . 3 ⊢ 𝜓
3	2	biantrur 530	. 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒))
4	1, 3	bitr4i 278	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpbiran2  710  mpbir2an  711  pm5.63  1021  equsexALT  2418  velcomp  3915  ddif  4089  dfun2  4218  dfin2  4219  0pss  4395  pssv  4397  disj4  4407  pwpwab  5049  zfpair  5357  opabn0  5491  relop  5788  ssrnres  6122  funopab  6512  funcnv2  6545  fnres  6604  dffv2  6912  idref  7074  rnoprab  7446  suppssr  8120  frrlem9  8219  brwitnlem  8417  omeu  8495  naddcllem  8586  elixp  8823  dfsup2  9323  card2inf  9436  harndom  9443  dford2  9505  cantnfp1lem3  9565  cantnfp1  9566  cantnflem1  9574  ttrclresv  9602  tz9.12lem3  9674  djulf1o  9797  djurf1o  9798  dfac4  10005  dfac12a  10032  cflem  10128  cflemOLD  10129  cfsmolem  10153  dffin7-2  10281  dfacfin7  10282  brdom3  10411  iunfo  10422  gch3  10559  lbfzo0  13591  fzo1lb  13605  1elfzo1  13606  gcdcllem3  16404  1nprm  16582  cygctb  19797  expmhm  21366  expghm  21405  opsrtoslem2  21984  mat1dimelbas  22379  basdif0  22861  txdis1cn  23543  trfil2  23795  txflf  23914  clsnsg  24018  tgpconncomp  24021  perfdvf  25824  wilthlem3  27000  noeta2  27717  ssltsnb  27725  etasslt2  27748  made0  27811  bdayon  28202  noseqind  28215  zsoring  28325  mptelee  28866  iscplgr  29386  rgrprcx  29564  blocnilem  30774  h1de2i  31523  nmop0  31956  nmfn0  31957  lnopconi  32004  lnfnconi  32025  stcltr2i  32245  funcnvmpt  32639  1stpreima  32678  2ndpreima  32679  suppss3  32696  onvf1od  35119  fmla0  35394  fmlasuc0  35396  elmrsubrn  35532  dftr6  35763  br6  35769  dford5reg  35795  txpss3v  35891  brtxp  35893  brpprod  35898  brsset  35902  dfon3  35905  brtxpsd  35907  brtxpsd2  35908  dffun10  35927  elfuns  35928  funpartlem  35955  fullfunfv  35960  dfrdg4  35964  dfint3  35965  brub  35967  hfext  36196  neibastop2lem  36373  bj-equsexval  36673  bj-elid3  37180  finxp0  37404  finxp1o  37405  brvdif  38275  xrnss3v  38379  ntrneiel2  44098  ntrneik4w  44112  ismnushort  44313  permaxpow  45021  funressnvmo  47055  dfdfat2  47138