Theorem mpbiran 973

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 267	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 196   ∧ 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 197  df-an 385

This theorem is referenced by:  mpbir2an  975  pm5.63  979  equsexvw  1978  equsexv  2147  equsexALT  2329  ddif  3775  dfun2  3892  dfin2  3893  0pss  4046  pssv  4049  disj4  4058  pwpwab  4646  zfpair  4934  opabn0  5035  relop  5305  ssrnres  5607  funopab  5961  funcnv2  5995  fnres  6045  dffv2  6310  idref  6539  rnoprab  6785  suppssr  7371  brwitnlem  7632  omeu  7710  elixp  7957  1sdom  8204  dfsup2  8391  wemapso2lem  8498  card2inf  8501  harndom  8510  dford2  8555  cantnfp1lem3  8615  cantnfp1  8616  cantnflem1  8624  tz9.12lem3  8690  dfac4  8983  dfac12a  9008  cflem  9106  cfsmolem  9130  dffin7-2  9258  dfacfin7  9259  brdom3  9388  iunfo  9399  gch3  9536  lbfzo0  12547  gcdcllem3  15270  1nprm  15439  cygctb  18339  opsrtoslem2  19533  expmhm  19863  expghm  19892  mat1dimelbas  20325  basdif0  20805  txdis1cn  21486  trfil2  21738  txflf  21857  clsnsg  21960  tgpconncomp  21963  perfdvf  23712  wilthlem3  24841  mptelee  25820  iscplgr  26366  rgrprcx  26544  blocnilem  27787  h1de2i  28540  nmop0  28973  nmfn0  28974  lnopconi  29021  lnfnconi  29042  stcltr2i  29262  funcnvmptOLD  29595  funcnvmpt  29596  1stpreima  29612  2ndpreima  29613  suppss3  29630  elmrsubrn  31543  dftr6  31766  dfpo2  31771  br6  31773  dford5reg  31811  txpss3v  32110  brsset  32121  dfon3  32124  brtxpsd  32126  brtxpsd2  32127  dffun10  32146  elfuns  32147  funpartlem  32174  fullfunfv  32179  dfrdg4  32183  dfint3  32184  brub  32186  hfext  32415  neibastop2lem  32480  bj-equsexval  32763  finxp0  33358  finxp1o  33359  brvdif  34166  xrnss3v  34274  ntrneiel2  38701  ntrneik4w  38715  compel  38958  dfdfat2  41532