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  1022  equsexALT  2424  velcomp  3966  ddif  4141  dfun2  4270  dfin2  4271  0pss  4447  pssv  4449  disj4  4459  pwpwab  5103  zfpair  5421  opabn0  5558  relop  5861  ssrnres  6198  funopab  6601  funcnv2  6634  fnres  6695  dffv2  7004  idref  7166  rnoprab  7538  suppssr  8220  frrlem9  8319  brwitnlem  8545  omeu  8623  naddcllem  8714  elixp  8944  1sdomOLD  9285  dfsup2  9484  card2inf  9595  harndom  9602  dford2  9660  cantnfp1lem3  9720  cantnfp1  9721  cantnflem1  9729  ttrclresv  9757  tz9.12lem3  9829  djulf1o  9952  djurf1o  9953  dfac4  10162  dfac12a  10189  cflem  10285  cflemOLD  10286  cfsmolem  10310  dffin7-2  10438  dfacfin7  10439  brdom3  10568  iunfo  10579  gch3  10716  lbfzo0  13739  fzo1lb  13753  gcdcllem3  16538  1nprm  16716  cygctb  19910  expmhm  21454  expghm  21486  opsrtoslem2  22080  mat1dimelbas  22477  basdif0  22960  txdis1cn  23643  trfil2  23895  txflf  24014  clsnsg  24118  tgpconncomp  24121  perfdvf  25938  wilthlem3  27113  noeta2  27829  etasslt2  27859  made0  27912  noseqind  28298  mptelee  28910  iscplgr  29432  rgrprcx  29610  blocnilem  30823  h1de2i  31572  nmop0  32005  nmfn0  32006  lnopconi  32053  lnfnconi  32074  stcltr2i  32294  funcnvmpt  32677  1stpreima  32716  2ndpreima  32717  suppss3  32735  fmla0  35387  fmlasuc0  35389  elmrsubrn  35525  dftr6  35751  br6  35757  dford5reg  35783  txpss3v  35879  brtxp  35881  brpprod  35886  brsset  35890  dfon3  35893  brtxpsd  35895  brtxpsd2  35896  dffun10  35915  elfuns  35916  funpartlem  35943  fullfunfv  35948  dfrdg4  35952  dfint3  35953  brub  35955  hfext  36184  neibastop2lem  36361  bj-equsexval  36661  bj-elid3  37168  finxp0  37392  finxp1o  37393  brvdif  38262  xrnss3v  38373  ntrneiel2  44099  ntrneik4w  44113  ismnushort  44320  funressnvmo  47057  dfdfat2  47140