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  5364  opabn0  5508  relop  5806  ssrnres  6143  funopab  6534  funcnv2  6567  fnres  6626  dffv2  6936  funcnvmpt  6950  idref  7100  rnoprab  7472  suppssr  8145  frrlem9  8244  brwitnlem  8442  omeu  8520  naddcllem  8612  elixp  8852  dfsup2  9357  card2inf  9470  harndom  9477  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  13654  fzo1lb  13668  1elfzo1  13669  gcdcllem3  16470  1nprm  16648  cygctb  19867  expmhm  21416  expghm  21455  opsrtoslem2  22034  mat1dimelbas  22436  basdif0  22918  txdis1cn  23600  trfil2  23852  txflf  23971  clsnsg  24075  tgpconncomp  24078  perfdvf  25870  wilthlem3  27033  noeta2  27753  sltssnb  27761  etaslts2  27786  made0  27855  bdayons  28268  noseqind  28284  zsoring  28401  mpteleeOLD  28964  iscplgr  29484  rgrprcx  29661  blocnilem  30875  h1de2i  31624  nmop0  32057  nmfn0  32058  lnopconi  32105  lnfnconi  32126  stcltr2i  32346  1stpreima  32780  2ndpreima  32781  suppss3  32796  onvf1od  35289  fmla0  35564  fmlasuc0  35566  elmrsubrn  35702  dftr6  35933  br6  35939  dford5reg  35962  txpss3v  36058  brtxp  36060  brpprod  36065  brsset  36069  dfon3  36072  brtxpsd  36074  brtxpsd2  36075  dffun10  36094  elfuns  36095  funpartlem  36124  fullfunfv  36129  dfrdg4  36133  dfint3  36134  brub  36136  hfext  36365  neibastop2lem  36542  bj-equsexval  36954  bj-elid3  37481  finxp0  37707  finxp1o  37708  brvdif  38587  xrnss3v  38702  ntrneiel2  44513  ntrneik4w  44527  ismnushort  44728  permaxpow  45436  funressnvmo  47487  dfdfat2  47570