Theorem mpbiran 955

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

Syntax hints:   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mpbir2an  957  pm5.63  961  equsexvw  1919  equsexv  2095  equsexALT  2282  ddif  3704  dfun2  3821  dfin2  3822  0pss  3965  pssv  3968  disj4  3977  zfpair  4831  opabn0  4931  relop  5194  ssrnres  5491  funopab  5837  funcnv2  5871  fnres  5921  dffv2  6181  idref  6403  rnoprab  6641  suppssr  7213  brwitnlem  7474  omeu  7552  elixp  7801  1sdom  8048  dfsup2  8233  wemapso2lem  8340  card2inf  8343  harndom  8352  dford2  8400  cantnfp1lem3  8460  cantnfp1  8461  cantnflem1  8469  tz9.12lem3  8535  dfac4  8828  dfac12a  8853  cflem  8951  cfsmolem  8975  dffin7-2  9103  dfacfin7  9104  brdom3  9231  iunfo  9240  gch3  9377  lbfzo0  12375  gcdcllem3  15061  1nprm  15230  cygctb  18116  opsrtoslem2  19306  expmhm  19634  expghm  19663  mat1dimelbas  20096  basdif0  20568  txdis1cn  21248  trfil2  21501  txflf  21620  clsnsg  21723  tgpconcomp  21726  perfdvf  23473  wilthlem3  24596  mptelee  25575  blocnilem  27043  h1de2i  27796  nmop0  28229  nmfn0  28230  lnopconi  28277  lnfnconi  28298  stcltr2i  28518  funcnvmptOLD  28850  funcnvmpt  28851  1stpreima  28867  2ndpreima  28868  suppss3  28890  elmrsubrn  30671  dftr6  30893  dfpo2  30898  br6  30900  dford5reg  30931  txpss3v  31155  brsset  31166  dfon3  31169  brtxpsd  31171  brtxpsd2  31172  dffun10  31191  elfuns  31192  funpartlem  31219  fullfunfv  31224  dfrdg4  31228  dfint3  31229  brub  31231  hfext  31460  neibastop2lem  31525  bj-equsexval  31827  finxp0  32404  finxp1o  32405  ntrneiel2  37404  ntrneik4w  37418  compel  37663  dfdfat2  39860  rgrprcx  40792