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  2418  velcomp  3932  ddif  4107  dfun2  4236  dfin2  4237  0pss  4413  pssv  4415  disj4  4425  pwpwab  5070  zfpair  5379  opabn0  5516  relop  5817  ssrnres  6154  funopab  6554  funcnv2  6587  fnres  6648  dffv2  6959  idref  7121  rnoprab  7497  suppssr  8177  frrlem9  8276  brwitnlem  8474  omeu  8552  naddcllem  8643  elixp  8880  1sdomOLD  9203  dfsup2  9402  card2inf  9515  harndom  9522  dford2  9580  cantnfp1lem3  9640  cantnfp1  9641  cantnflem1  9649  ttrclresv  9677  tz9.12lem3  9749  djulf1o  9872  djurf1o  9873  dfac4  10082  dfac12a  10109  cflem  10205  cflemOLD  10206  cfsmolem  10230  dffin7-2  10358  dfacfin7  10359  brdom3  10488  iunfo  10499  gch3  10636  lbfzo0  13667  fzo1lb  13681  1elfzo1  13682  gcdcllem3  16478  1nprm  16656  cygctb  19829  expmhm  21360  expghm  21392  opsrtoslem2  21970  mat1dimelbas  22365  basdif0  22847  txdis1cn  23529  trfil2  23781  txflf  23900  clsnsg  24004  tgpconncomp  24007  perfdvf  25811  wilthlem3  26987  noeta2  27703  etasslt2  27733  made0  27792  bdayon  28180  noseqind  28193  mptelee  28829  iscplgr  29349  rgrprcx  29527  blocnilem  30740  h1de2i  31489  nmop0  31922  nmfn0  31923  lnopconi  31970  lnfnconi  31991  stcltr2i  32211  funcnvmpt  32598  1stpreima  32637  2ndpreima  32638  suppss3  32654  onvf1od  35101  fmla0  35376  fmlasuc0  35378  elmrsubrn  35514  dftr6  35745  br6  35751  dford5reg  35777  txpss3v  35873  brtxp  35875  brpprod  35880  brsset  35884  dfon3  35887  brtxpsd  35889  brtxpsd2  35890  dffun10  35909  elfuns  35910  funpartlem  35937  fullfunfv  35942  dfrdg4  35946  dfint3  35947  brub  35949  hfext  36178  neibastop2lem  36355  bj-equsexval  36655  bj-elid3  37162  finxp0  37386  finxp1o  37387  brvdif  38257  xrnss3v  38361  ntrneiel2  44082  ntrneik4w  44096  ismnushort  44297  permaxpow  45006  funressnvmo  47050  dfdfat2  47133