Theorem mpbiran 709

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  710  mpbir2an  711  pm5.63  1021  equsexALT  2421  velcomp  3977  ddif  4150  dfun2  4275  dfin2  4276  0pss  4452  pssv  4454  disj4  4464  pwpwab  5107  zfpair  5426  opabn0  5562  relop  5863  ssrnres  6199  funopab  6602  funcnv2  6635  fnres  6695  dffv2  7003  idref  7165  rnoprab  7536  suppssr  8218  frrlem9  8317  brwitnlem  8543  omeu  8621  naddcllem  8712  elixp  8942  1sdomOLD  9282  dfsup2  9481  card2inf  9592  harndom  9599  dford2  9657  cantnfp1lem3  9717  cantnfp1  9718  cantnflem1  9726  ttrclresv  9754  tz9.12lem3  9826  djulf1o  9949  djurf1o  9950  dfac4  10159  dfac12a  10186  cflem  10282  cflemOLD  10283  cfsmolem  10307  dffin7-2  10435  dfacfin7  10436  brdom3  10565  iunfo  10576  gch3  10713  lbfzo0  13735  fzo1lb  13749  gcdcllem3  16534  1nprm  16712  cygctb  19924  expmhm  21471  expghm  21503  opsrtoslem2  22097  mat1dimelbas  22492  basdif0  22975  txdis1cn  23658  trfil2  23910  txflf  24029  clsnsg  24133  tgpconncomp  24136  perfdvf  25952  wilthlem3  27127  noeta2  27843  etasslt2  27873  made0  27926  noseqind  28312  mptelee  28924  iscplgr  29446  rgrprcx  29624  blocnilem  30832  h1de2i  31581  nmop0  32014  nmfn0  32015  lnopconi  32062  lnfnconi  32083  stcltr2i  32303  funcnvmpt  32683  1stpreima  32721  2ndpreima  32722  suppss3  32741  fmla0  35366  fmlasuc0  35368  elmrsubrn  35504  dftr6  35730  br6  35736  dford5reg  35763  txpss3v  35859  brtxp  35861  brpprod  35866  brsset  35870  dfon3  35873  brtxpsd  35875  brtxpsd2  35876  dffun10  35895  elfuns  35896  funpartlem  35923  fullfunfv  35928  dfrdg4  35932  dfint3  35933  brub  35935  hfext  36164  neibastop2lem  36342  bj-equsexval  36642  bj-elid3  37149  finxp0  37373  finxp1o  37374  brvdif  38242  xrnss3v  38353  ntrneiel2  44075  ntrneik4w  44089  ismnushort  44296  funressnvmo  46994  dfdfat2  47077