Theorem mpbiran 702

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

Syntax hints:   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  mpbir2an  704  pm5.63  1050  equsexvw  2111  equsexv  2301  equsexALT  2439  ddif  3968  dfun2  4088  dfin2  4089  0pss  4237  pssv  4239  disj4  4249  pwpwab  4834  zfpair  5124  opabn0  5231  relop  5504  ssrnres  5812  funopab  6157  funcnv2  6189  fnres  6239  dffv2  6517  idref  6661  rnoprab  7002  suppssr  7590  brwitnlem  7853  omeu  7931  elixp  8181  1sdom  8431  dfsup2  8618  wemapso2lem  8725  card2inf  8728  harndom  8737  dford2  8793  cantnfp1lem3  8853  cantnfp1  8854  cantnflem1  8862  tz9.12lem3  8928  djulf1o  9050  djurf1o  9051  dfac4  9257  dfac12a  9284  cflem  9382  cfsmolem  9406  dffin7-2  9534  dfacfin7  9535  brdom3  9664  iunfo  9675  gch3  9812  lbfzo0  12802  gcdcllem3  15595  1nprm  15763  cygctb  18645  opsrtoslem2  19844  expmhm  20174  expghm  20203  mat1dimelbas  20644  basdif0  21127  txdis1cn  21808  trfil2  22060  txflf  22179  clsnsg  22282  tgpconncomp  22285  perfdvf  24065  wilthlem3  25208  mptelee  26193  iscplgr  26712  rgrprcx  26889  blocnilem  28213  h1de2i  28966  nmop0  29399  nmfn0  29400  lnopconi  29447  lnfnconi  29468  stcltr2i  29688  funcnvmpt  30015  1stpreima  30031  2ndpreima  30032  suppss3  30049  elmrsubrn  31962  dftr6  32181  br6  32188  dford5reg  32224  txpss3v  32523  brtxp  32525  brpprod  32530  brsset  32534  dfon3  32537  brtxpsd  32539  brtxpsd2  32540  dffun10  32559  elfuns  32560  funpartlem  32587  fullfunfv  32592  dfrdg4  32596  dfint3  32597  brub  32599  hfext  32828  neibastop2lem  32892  bj-equsexval  33173  bj-elid4  33615  finxp0  33772  finxp1o  33773  brvdif  34578  xrnss3v  34681  ntrneiel2  39223  ntrneik4w  39237  compel  39479  funressnvmo  41975  dfdfat2  42029