Theorem mpbiran 709

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpbiran2  710  mpbir2an  711  pm5.63  1021  equsexALT  2417  velcomp  3929  ddif  4104  dfun2  4233  dfin2  4234  0pss  4410  pssv  4412  disj4  4422  pwpwab  5067  zfpair  5376  opabn0  5513  relop  5814  ssrnres  6151  funopab  6551  funcnv2  6584  fnres  6645  dffv2  6956  idref  7118  rnoprab  7494  suppssr  8174  frrlem9  8273  brwitnlem  8471  omeu  8549  naddcllem  8640  elixp  8877  1sdomOLD  9196  dfsup2  9395  card2inf  9508  harndom  9515  dford2  9573  cantnfp1lem3  9633  cantnfp1  9634  cantnflem1  9642  ttrclresv  9670  tz9.12lem3  9742  djulf1o  9865  djurf1o  9866  dfac4  10075  dfac12a  10102  cflem  10198  cflemOLD  10199  cfsmolem  10223  dffin7-2  10351  dfacfin7  10352  brdom3  10481  iunfo  10492  gch3  10629  lbfzo0  13660  fzo1lb  13674  1elfzo1  13675  gcdcllem3  16471  1nprm  16649  cygctb  19822  expmhm  21353  expghm  21385  opsrtoslem2  21963  mat1dimelbas  22358  basdif0  22840  txdis1cn  23522  trfil2  23774  txflf  23893  clsnsg  23997  tgpconncomp  24000  perfdvf  25804  wilthlem3  26980  noeta2  27696  etasslt2  27726  made0  27785  bdayon  28173  noseqind  28186  mptelee  28822  iscplgr  29342  rgrprcx  29520  blocnilem  30733  h1de2i  31482  nmop0  31915  nmfn0  31916  lnopconi  31963  lnfnconi  31984  stcltr2i  32204  funcnvmpt  32591  1stpreima  32630  2ndpreima  32631  suppss3  32647  onvf1od  35094  fmla0  35369  fmlasuc0  35371  elmrsubrn  35507  dftr6  35738  br6  35744  dford5reg  35770  txpss3v  35866  brtxp  35868  brpprod  35873  brsset  35877  dfon3  35880  brtxpsd  35882  brtxpsd2  35883  dffun10  35902  elfuns  35903  funpartlem  35930  fullfunfv  35935  dfrdg4  35939  dfint3  35940  brub  35942  hfext  36171  neibastop2lem  36348  bj-equsexval  36648  bj-elid3  37155  finxp0  37379  finxp1o  37380  brvdif  38250  xrnss3v  38354  ntrneiel2  44075  ntrneik4w  44089  ismnushort  44290  permaxpow  44999  funressnvmo  47046  dfdfat2  47129