Theorem mpbiran 708

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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  mpbiran2  709  mpbir2an  710  pm5.63  1019  equsexALT  2419  velcomp  3964  ddif  4137  dfun2  4260  dfin2  4261  0pss  4445  pssv  4447  disj4  4459  pwpwab  5107  zfpair  5420  opabn0  5554  relop  5851  ssrnres  6178  funopab  6584  funcnv2  6617  fnres  6678  dffv2  6987  idref  7144  rnoprab  7512  suppssr  8181  frrlem9  8279  brwitnlem  8507  omeu  8585  naddcllem  8675  elixp  8898  1sdomOLD  9249  dfsup2  9439  card2inf  9550  harndom  9557  dford2  9615  cantnfp1lem3  9675  cantnfp1  9676  cantnflem1  9684  ttrclresv  9712  tz9.12lem3  9784  djulf1o  9907  djurf1o  9908  dfac4  10117  dfac12a  10143  cflem  10241  cfsmolem  10265  dffin7-2  10393  dfacfin7  10394  brdom3  10523  iunfo  10534  gch3  10671  lbfzo0  13672  gcdcllem3  16442  1nprm  16616  cygctb  19760  expmhm  21014  expghm  21045  opsrtoslem2  21617  mat1dimelbas  21973  basdif0  22456  txdis1cn  23139  trfil2  23391  txflf  23510  clsnsg  23614  tgpconncomp  23617  perfdvf  25420  wilthlem3  26574  noeta2  27286  etasslt2  27315  made0  27368  mptelee  28153  iscplgr  28672  rgrprcx  28849  blocnilem  30057  h1de2i  30806  nmop0  31239  nmfn0  31240  lnopconi  31287  lnfnconi  31308  stcltr2i  31528  funcnvmpt  31892  1stpreima  31928  2ndpreima  31929  suppss3  31949  fmla0  34373  fmlasuc0  34375  elmrsubrn  34511  dftr6  34721  br6  34727  dford5reg  34754  txpss3v  34850  brtxp  34852  brpprod  34857  brsset  34861  dfon3  34864  brtxpsd  34866  brtxpsd2  34867  dffun10  34886  elfuns  34887  funpartlem  34914  fullfunfv  34919  dfrdg4  34923  dfint3  34924  brub  34926  hfext  35155  neibastop2lem  35245  bj-equsexval  35537  bj-elid3  36048  finxp0  36272  finxp1o  36273  brvdif  37129  xrnss3v  37242  ntrneiel2  42837  ntrneik4w  42851  ismnushort  43060  funressnvmo  45755  dfdfat2  45836