Theorem mpbiran 705

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 529	. 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒))
4	1, 3	bitr4i 277	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  mpbiran2  706  mpbir2an  707  pm5.63  1016  equsexALT  2416  velcomp  3962  ddif  4135  dfun2  4258  dfin2  4259  0pss  4443  pssv  4445  disj4  4457  pwpwab  5105  zfpair  5418  opabn0  5552  relop  5849  ssrnres  6176  funopab  6582  funcnv2  6615  fnres  6676  dffv2  6985  idref  7145  rnoprab  7514  suppssr  8183  frrlem9  8281  brwitnlem  8509  omeu  8587  naddcllem  8677  elixp  8900  1sdomOLD  9251  dfsup2  9441  card2inf  9552  harndom  9559  dford2  9617  cantnfp1lem3  9677  cantnfp1  9678  cantnflem1  9686  ttrclresv  9714  tz9.12lem3  9786  djulf1o  9909  djurf1o  9910  dfac4  10119  dfac12a  10145  cflem  10243  cfsmolem  10267  dffin7-2  10395  dfacfin7  10396  brdom3  10525  iunfo  10536  gch3  10673  lbfzo0  13676  gcdcllem3  16446  1nprm  16620  cygctb  19801  expmhm  21214  expghm  21246  opsrtoslem2  21836  mat1dimelbas  22193  basdif0  22676  txdis1cn  23359  trfil2  23611  txflf  23730  clsnsg  23834  tgpconncomp  23837  perfdvf  25652  wilthlem3  26810  noeta2  27522  etasslt2  27552  made0  27605  mptelee  28420  iscplgr  28939  rgrprcx  29116  blocnilem  30324  h1de2i  31073  nmop0  31506  nmfn0  31507  lnopconi  31554  lnfnconi  31575  stcltr2i  31795  funcnvmpt  32159  1stpreima  32195  2ndpreima  32196  suppss3  32216  fmla0  34671  fmlasuc0  34673  elmrsubrn  34809  dftr6  35025  br6  35031  dford5reg  35058  txpss3v  35154  brtxp  35156  brpprod  35161  brsset  35165  dfon3  35168  brtxpsd  35170  brtxpsd2  35171  dffun10  35190  elfuns  35191  funpartlem  35218  fullfunfv  35223  dfrdg4  35227  dfint3  35228  brub  35230  hfext  35459  neibastop2lem  35548  bj-equsexval  35840  bj-elid3  36351  finxp0  36575  finxp1o  36576  brvdif  37432  xrnss3v  37545  ntrneiel2  43139  ntrneik4w  43153  ismnushort  43362  funressnvmo  46053  dfdfat2  46134