Theorem mpbiran 710

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  711  mpbir2an  712  pm5.63  1022  equsexALT  2424  velcomp  3917  ddif  4094  dfun2  4223  dfin2  4224  0pss  4400  pssv  4402  disj4  4412  pwpwab  5059  zfpair  5367  opabn0  5502  relop  5800  ssrnres  6137  funopab  6528  funcnv2  6561  fnres  6620  dffv2  6930  funcnvmpt  6944  idref  7093  rnoprab  7465  suppssr  8139  frrlem9  8238  brwitnlem  8436  omeu  8514  naddcllem  8606  elixp  8846  dfsup2  9351  card2inf  9464  harndom  9471  dford2  9533  cantnfp1lem3  9593  cantnfp1  9594  cantnflem1  9602  ttrclresv  9630  tz9.12lem3  9705  djulf1o  9828  djurf1o  9829  dfac4  10036  dfac12a  10063  cflem  10159  cflemOLD  10160  cfsmolem  10184  dffin7-2  10312  dfacfin7  10313  brdom3  10442  iunfo  10453  gch3  10591  lbfzo0  13619  fzo1lb  13633  1elfzo1  13634  gcdcllem3  16432  1nprm  16610  cygctb  19825  expmhm  21395  expghm  21434  opsrtoslem2  22015  mat1dimelbas  22419  basdif0  22901  txdis1cn  23583  trfil2  23835  txflf  23954  clsnsg  24058  tgpconncomp  24061  perfdvf  25864  wilthlem3  27040  noeta2  27761  ssltsnb  27769  etasslt2  27792  made0  27855  bdayon  28257  noseqind  28273  zsoring  28388  mpteleeOLD  28951  iscplgr  29471  rgrprcx  29649  blocnilem  30862  h1de2i  31611  nmop0  32044  nmfn0  32045  lnopconi  32092  lnfnconi  32113  stcltr2i  32333  1stpreima  32767  2ndpreima  32768  suppss3  32783  onvf1od  35282  fmla0  35557  fmlasuc0  35559  elmrsubrn  35695  dftr6  35926  br6  35932  dford5reg  35955  txpss3v  36051  brtxp  36053  brpprod  36058  brsset  36062  dfon3  36065  brtxpsd  36067  brtxpsd2  36068  dffun10  36087  elfuns  36088  funpartlem  36117  fullfunfv  36122  dfrdg4  36126  dfint3  36127  brub  36129  hfext  36358  neibastop2lem  36535  bj-equsexval  36836  bj-elid3  37343  finxp0  37567  finxp1o  37568  brvdif  38438  xrnss3v  38553  ntrneiel2  44363  ntrneik4w  44377  ismnushort  44578  permaxpow  45286  funressnvmo  47327  dfdfat2  47410