Theorem mpbiran 710

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  711  mpbir2an  712  pm5.63  1022  equsexALT  2424  velcomp  3905  ddif  4082  dfun2  4211  dfin2  4212  0pss  4388  pssv  4390  disj4  4400  pwpwab  5046  zfpair  5356  opabn0  5499  relop  5797  ssrnres  6134  funopab  6525  funcnv2  6558  fnres  6617  dffv2  6927  funcnvmpt  6941  idref  7091  rnoprab  7463  suppssr  8136  frrlem9  8235  brwitnlem  8433  omeu  8511  naddcllem  8603  elixp  8843  dfsup2  9348  card2inf  9461  harndom  9468  dford2  9530  cantnfp1lem3  9590  cantnfp1  9591  cantnflem1  9599  ttrclresv  9627  tz9.12lem3  9702  djulf1o  9825  djurf1o  9826  dfac4  10033  dfac12a  10060  cflem  10156  cflemOLD  10157  cfsmolem  10181  dffin7-2  10309  dfacfin7  10310  brdom3  10439  iunfo  10450  gch3  10588  lbfzo0  13643  fzo1lb  13657  1elfzo1  13658  gcdcllem3  16459  1nprm  16637  cygctb  19856  expmhm  21424  expghm  21463  opsrtoslem2  22043  mat1dimelbas  22445  basdif0  22927  txdis1cn  23609  trfil2  23861  txflf  23980  clsnsg  24084  tgpconncomp  24087  perfdvf  25879  wilthlem3  27051  noeta2  27772  sltssnb  27780  etaslts2  27805  made0  27874  bdayons  28287  noseqind  28303  zsoring  28420  mpteleeOLD  28983  iscplgr  29503  rgrprcx  29681  blocnilem  30895  h1de2i  31644  nmop0  32077  nmfn0  32078  lnopconi  32125  lnfnconi  32146  stcltr2i  32366  1stpreima  32800  2ndpreima  32801  suppss3  32816  onvf1od  35310  fmla0  35585  fmlasuc0  35587  elmrsubrn  35723  dftr6  35954  br6  35960  dford5reg  35983  txpss3v  36079  brtxp  36081  brpprod  36086  brsset  36090  dfon3  36093  brtxpsd  36095  brtxpsd2  36096  dffun10  36115  elfuns  36116  funpartlem  36145  fullfunfv  36150  dfrdg4  36154  dfint3  36155  brub  36157  hfext  36386  neibastop2lem  36563  bj-equsexval  36967  bj-elid3  37494  finxp0  37718  finxp1o  37719  brvdif  38598  xrnss3v  38713  ntrneiel2  44528  ntrneik4w  44542  ismnushort  44743  permaxpow  45451  funressnvmo  47490  dfdfat2  47573