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  3918  ddif  4095  dfun2  4224  dfin2  4225  0pss  4401  pssv  4403  disj4  4413  pwpwab  5060  zfpair  5368  opabn0  5509  relop  5807  ssrnres  6144  funopab  6535  funcnv2  6568  fnres  6627  dffv2  6937  funcnvmpt  6951  idref  7101  rnoprab  7473  suppssr  8147  frrlem9  8246  brwitnlem  8444  omeu  8522  naddcllem  8614  elixp  8854  dfsup2  9359  card2inf  9472  harndom  9479  dford2  9541  cantnfp1lem3  9601  cantnfp1  9602  cantnflem1  9610  ttrclresv  9638  tz9.12lem3  9713  djulf1o  9836  djurf1o  9837  dfac4  10044  dfac12a  10071  cflem  10167  cflemOLD  10168  cfsmolem  10192  dffin7-2  10320  dfacfin7  10321  brdom3  10450  iunfo  10461  gch3  10599  lbfzo0  13627  fzo1lb  13641  1elfzo1  13642  gcdcllem3  16440  1nprm  16618  cygctb  19833  expmhm  21403  expghm  21442  opsrtoslem2  22023  mat1dimelbas  22427  basdif0  22909  txdis1cn  23591  trfil2  23843  txflf  23962  clsnsg  24066  tgpconncomp  24069  perfdvf  25872  wilthlem3  27048  noeta2  27769  sltssnb  27777  etaslts2  27802  made0  27871  bdayons  28284  noseqind  28300  zsoring  28417  mpteleeOLD  28980  iscplgr  29500  rgrprcx  29678  blocnilem  30891  h1de2i  31640  nmop0  32073  nmfn0  32074  lnopconi  32121  lnfnconi  32142  stcltr2i  32362  1stpreima  32796  2ndpreima  32797  suppss3  32812  onvf1od  35320  fmla0  35595  fmlasuc0  35597  elmrsubrn  35733  dftr6  35964  br6  35970  dford5reg  35993  txpss3v  36089  brtxp  36091  brpprod  36096  brsset  36100  dfon3  36103  brtxpsd  36105  brtxpsd2  36106  dffun10  36125  elfuns  36126  funpartlem  36155  fullfunfv  36160  dfrdg4  36164  dfint3  36165  brub  36167  hfext  36396  neibastop2lem  36573  bj-equsexval  36898  bj-elid3  37411  finxp0  37635  finxp1o  37636  brvdif  38506  xrnss3v  38621  ntrneiel2  44431  ntrneik4w  44445  ismnushort  44646  permaxpow  45354  funressnvmo  47394  dfdfat2  47477