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  2421  velcomp  3914  ddif  4092  dfun2  4221  dfin2  4222  0pss  4398  pssv  4400  disj4  4410  pwpwab  5055  zfpair  5363  opabn0  5498  relop  5797  ssrnres  6133  funopab  6524  funcnv2  6557  fnres  6616  dffv2  6926  idref  7088  rnoprab  7460  suppssr  8134  frrlem9  8233  brwitnlem  8431  omeu  8509  naddcllem  8600  elixp  8837  dfsup2  9338  card2inf  9451  harndom  9458  dford2  9520  cantnfp1lem3  9580  cantnfp1  9581  cantnflem1  9589  ttrclresv  9617  tz9.12lem3  9692  djulf1o  9815  djurf1o  9816  dfac4  10023  dfac12a  10050  cflem  10146  cflemOLD  10147  cfsmolem  10171  dffin7-2  10299  dfacfin7  10300  brdom3  10429  iunfo  10440  gch3  10577  lbfzo0  13609  fzo1lb  13623  1elfzo1  13624  gcdcllem3  16422  1nprm  16600  cygctb  19814  expmhm  21383  expghm  21422  opsrtoslem2  22001  mat1dimelbas  22396  basdif0  22878  txdis1cn  23560  trfil2  23812  txflf  23931  clsnsg  24035  tgpconncomp  24038  perfdvf  25841  wilthlem3  27017  noeta2  27734  ssltsnb  27742  etasslt2  27765  made0  27828  bdayon  28219  noseqind  28232  zsoring  28342  mpteleeOLD  28884  iscplgr  29404  rgrprcx  29582  blocnilem  30795  h1de2i  31544  nmop0  31977  nmfn0  31978  lnopconi  32025  lnfnconi  32046  stcltr2i  32266  funcnvmpt  32660  1stpreima  32699  2ndpreima  32700  suppss3  32717  onvf1od  35162  fmla0  35437  fmlasuc0  35439  elmrsubrn  35575  dftr6  35806  br6  35812  dford5reg  35835  txpss3v  35931  brtxp  35933  brpprod  35938  brsset  35942  dfon3  35945  brtxpsd  35947  brtxpsd2  35948  dffun10  35967  elfuns  35968  funpartlem  35997  fullfunfv  36002  dfrdg4  36006  dfint3  36007  brub  36009  hfext  36238  neibastop2lem  36415  bj-equsexval  36715  bj-elid3  37222  finxp0  37446  finxp1o  37447  brvdif  38308  xrnss3v  38415  ntrneiel2  44193  ntrneik4w  44207  ismnushort  44408  permaxpow  45116  funressnvmo  47159  dfdfat2  47242