Theorem mpbiran 708

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  mpbiran2  709  mpbir2an  710  pm5.63  1017  equsexvwOLD  2012  equsexv  2266  equsexALT  2430  velcomp  3896  ddif  4064  dfun2  4186  dfin2  4187  0pss  4352  pssv  4354  disj4  4366  pwpwab  4988  zfpair  5287  opabn0  5405  relop  5685  ssrnres  6002  funopab  6359  funcnv2  6392  fnres  6446  dffv2  6733  idref  6885  rnoprab  7236  suppssr  7844  brwitnlem  8115  omeu  8194  elixp  8451  1sdom  8705  dfsup2  8892  card2inf  9003  harndom  9010  dford2  9067  cantnfp1lem3  9127  cantnfp1  9128  cantnflem1  9136  tz9.12lem3  9202  djulf1o  9325  djurf1o  9326  dfac4  9533  dfac12a  9559  cflem  9657  cfsmolem  9681  dffin7-2  9809  dfacfin7  9810  brdom3  9939  iunfo  9950  gch3  10087  lbfzo0  13072  gcdcllem3  15840  1nprm  16013  cygctb  19005  expmhm  20160  expghm  20189  opsrtoslem2  20724  mat1dimelbas  21076  basdif0  21558  txdis1cn  22240  trfil2  22492  txflf  22611  clsnsg  22715  tgpconncomp  22718  perfdvf  24506  wilthlem3  25655  mptelee  26689  iscplgr  27205  rgrprcx  27382  blocnilem  28587  h1de2i  29336  nmop0  29769  nmfn0  29770  lnopconi  29817  lnfnconi  29838  stcltr2i  30058  funcnvmpt  30430  1stpreima  30466  2ndpreima  30467  suppss3  30486  fmla0  32742  fmlasuc0  32744  elmrsubrn  32880  dftr6  33099  br6  33106  dford5reg  33140  frrlem9  33244  txpss3v  33452  brtxp  33454  brpprod  33459  brsset  33463  dfon3  33466  brtxpsd  33468  brtxpsd2  33469  dffun10  33488  elfuns  33489  funpartlem  33516  fullfunfv  33521  dfrdg4  33525  dfint3  33526  brub  33528  hfext  33757  neibastop2lem  33821  bj-equsexval  34106  bj-elid3  34582  finxp0  34808  finxp1o  34809  brvdif  35682  xrnss3v  35784  ntrneiel2  40789  ntrneik4w  40803  funressnvmo  43637  dfdfat2  43684