Theorem mpbiran 954

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

Syntax hints:   ↔ wb 194   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  mpbir2an  956  pm5.63  960  equsexvw  1918  equsexv  2094  equsexALT  2281  ddif  3703  dfun2  3820  dfin2  3821  0pss  3964  pssv  3967  disj4  3976  zfpair  4826  opabn0  4921  relop  5182  ssrnres  5477  funopab  5823  funcnv2  5857  fnres  5907  dffv2  6166  idref  6381  rnoprab  6619  suppssr  7191  brwitnlem  7452  omeu  7530  elixp  7779  1sdom  8026  dfsup2  8211  wemapso2lem  8318  card2inf  8321  harndom  8330  dford2  8378  cantnfp1lem3  8438  cantnfp1  8439  cantnflem1  8447  tz9.12lem3  8513  dfac4  8806  dfac12a  8831  cflem  8929  cfsmolem  8953  dffin7-2  9081  dfacfin7  9082  brdom3  9209  iunfo  9218  gch3  9355  lbfzo0  12333  gcdcllem3  15010  1nprm  15179  cygctb  18065  opsrtoslem2  19255  expmhm  19583  expghm  19611  mat1dimelbas  20044  basdif0  20516  txdis1cn  21196  trfil2  21449  txflf  21568  clsnsg  21671  tgpconcomp  21674  perfdvf  23418  wilthlem3  24541  mptelee  25521  blocnilem  26877  h1de2i  27630  nmop0  28063  nmfn0  28064  lnopconi  28111  lnfnconi  28132  stcltr2i  28352  funcnvmptOLD  28684  funcnvmpt  28685  1stpreima  28701  2ndpreima  28702  suppss3  28724  elmrsubrn  30505  dftr6  30727  dfpo2  30732  br6  30734  dford5reg  30765  txpss3v  30989  brsset  31000  dfon3  31003  brtxpsd  31005  brtxpsd2  31006  dffun10  31025  elfuns  31026  funpartlem  31053  fullfunfv  31058  dfrdg4  31062  dfint3  31063  brub  31065  hfext  31294  neibastop2lem  31359  bj-equsexval  31661  finxp0  32228  finxp1o  32229  ntrneiel2  37228  ntrneik4w  37242  compel  37487  dfdfat2  39685  rgrprcx  40814