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  3905  0pss  4388  pssv  4390  disj4  4400  pwpwab  5046  zfpair  5356  opabn0  5499  relop  5797  ssrnres  6134  funopab  6525  funcnv2  6558  fnres  6617  dffv2  6927  funcnvmpt  6941  idref  7091  rnoprab  7463  suppssr  8136  frrlem9  8235  brwitnlem  8433  omeu  8511  naddcllem  8603  elixp  8843  dfsup2  9348  card2inf  9461  harndom  9468  dford2  9530  cantnfp1lem3  9590  cantnfp1  9591  cantnflem1  9599  ttrclresv  9627  tz9.12lem3  9702  djulf1o  9825  djurf1o  9826  dfac4  10033  dfac12a  10060  cflem  10156  cflemOLD  10157  cfsmolem  10181  dffin7-2  10309  dfacfin7  10310  brdom3  10439  iunfo  10450  gch3  10588  lbfzo0  13643  fzo1lb  13657  1elfzo1  13658  gcdcllem3  16459  1nprm  16637  cygctb  19856  expmhm  21424  expghm  21463  opsrtoslem2  22042  mat1dimelbas  22444  basdif0  22926  txdis1cn  23608  trfil2  23860  txflf  23979  clsnsg  24083  tgpconncomp  24086  perfdvf  25878  wilthlem3  27045  noeta2  27765  sltssnb  27773  etaslts2  27798  made0  27867  bdayons  28280  noseqind  28296  zsoring  28413  mpteleeOLD  28976  iscplgr  29496  rgrprcx  29674  blocnilem  30888  h1de2i  31637  nmop0  32070  nmfn0  32071  lnopconi  32118  lnfnconi  32139  stcltr2i  32359  1stpreima  32793  2ndpreima  32794  suppss3  32809  onvf1od  35303  fmla0  35578  fmlasuc0  35580  elmrsubrn  35716  dftr6  35947  br6  35953  dford5reg  35976  txpss3v  36072  brtxp  36074  brpprod  36079  brsset  36083  dfon3  36086  brtxpsd  36088  brtxpsd2  36089  dffun10  36108  elfuns  36109  funpartlem  36138  fullfunfv  36143  dfrdg4  36147  dfint3  36148  brub  36150  hfext  36379  neibastop2lem  36556  bj-equsexval  36960  bj-elid3  37487  finxp0  37711  finxp1o  37712  brvdif  38591  xrnss3v  38706  ntrneiel2  44521  ntrneik4w  44535  ismnushort  44736  permaxpow  45444  funressnvmo  47495  dfdfat2  47578