Theorem mpbiran 707

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpbiran2  708  mpbir2an  709  pm5.63  1016  equsexvwOLD  2008  equsexv  2264  equsexALT  2437  velcomp  3951  ddif  4113  dfun2  4236  dfin2  4237  0pss  4396  pssv  4398  disj4  4408  pwpwab  5018  zfpair  5314  opabn0  5433  relop  5716  ssrnres  6030  funopab  6385  funcnv2  6417  fnres  6469  dffv2  6751  idref  6903  rnoprab  7251  suppssr  7855  brwitnlem  8126  omeu  8205  elixp  8462  1sdom  8715  dfsup2  8902  card2inf  9013  harndom  9022  dford2  9077  cantnfp1lem3  9137  cantnfp1  9138  cantnflem1  9146  tz9.12lem3  9212  djulf1o  9335  djurf1o  9336  dfac4  9542  dfac12a  9568  cflem  9662  cfsmolem  9686  dffin7-2  9814  dfacfin7  9815  brdom3  9944  iunfo  9955  gch3  10092  lbfzo0  13071  gcdcllem3  15844  1nprm  16017  cygctb  19006  opsrtoslem2  20259  expmhm  20608  expghm  20637  mat1dimelbas  21074  basdif0  21555  txdis1cn  22237  trfil2  22489  txflf  22608  clsnsg  22712  tgpconncomp  22715  perfdvf  24495  wilthlem3  25641  mptelee  26675  iscplgr  27191  rgrprcx  27368  blocnilem  28575  h1de2i  29324  nmop0  29757  nmfn0  29758  lnopconi  29805  lnfnconi  29826  stcltr2i  30046  funcnvmpt  30406  1stpreima  30436  2ndpreima  30437  suppss3  30454  fmla0  32624  fmlasuc0  32626  elmrsubrn  32762  dftr6  32981  br6  32988  dford5reg  33022  frrlem9  33126  txpss3v  33334  brtxp  33336  brpprod  33341  brsset  33345  dfon3  33348  brtxpsd  33350  brtxpsd2  33351  dffun10  33370  elfuns  33371  funpartlem  33398  fullfunfv  33403  dfrdg4  33407  dfint3  33408  brub  33410  hfext  33639  neibastop2lem  33703  bj-equsexval  33988  bj-elid3  34453  finxp0  34666  finxp1o  34667  brvdif  35516  xrnss3v  35618  ntrneiel2  40429  ntrneik4w  40443  funressnvmo  43273  dfdfat2  43320