Theorem mpbiran 707

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  mpbiran2  708  mpbir2an  709  pm5.63  1018  equsexALT  2418  velcomp  3963  ddif  4136  dfun2  4259  dfin2  4260  0pss  4444  pssv  4446  disj4  4458  pwpwab  5106  zfpair  5419  opabn0  5553  relop  5850  ssrnres  6177  funopab  6583  funcnv2  6616  fnres  6677  dffv2  6986  idref  7143  rnoprab  7511  suppssr  8180  frrlem9  8278  brwitnlem  8506  omeu  8584  naddcllem  8674  elixp  8897  1sdomOLD  9248  dfsup2  9438  card2inf  9549  harndom  9556  dford2  9614  cantnfp1lem3  9674  cantnfp1  9675  cantnflem1  9683  ttrclresv  9711  tz9.12lem3  9783  djulf1o  9906  djurf1o  9907  dfac4  10116  dfac12a  10142  cflem  10240  cfsmolem  10264  dffin7-2  10392  dfacfin7  10393  brdom3  10522  iunfo  10533  gch3  10670  lbfzo0  13671  gcdcllem3  16441  1nprm  16615  cygctb  19759  expmhm  21013  expghm  21044  opsrtoslem2  21616  mat1dimelbas  21972  basdif0  22455  txdis1cn  23138  trfil2  23390  txflf  23509  clsnsg  23613  tgpconncomp  23616  perfdvf  25419  wilthlem3  26571  noeta2  27283  etasslt2  27312  made0  27365  mptelee  28150  iscplgr  28669  rgrprcx  28846  blocnilem  30052  h1de2i  30801  nmop0  31234  nmfn0  31235  lnopconi  31282  lnfnconi  31303  stcltr2i  31523  funcnvmpt  31887  1stpreima  31923  2ndpreima  31924  suppss3  31944  fmla0  34368  fmlasuc0  34370  elmrsubrn  34506  dftr6  34716  br6  34722  dford5reg  34749  txpss3v  34845  brtxp  34847  brpprod  34852  brsset  34856  dfon3  34859  brtxpsd  34861  brtxpsd2  34862  dffun10  34881  elfuns  34882  funpartlem  34909  fullfunfv  34914  dfrdg4  34918  dfint3  34919  brub  34921  hfext  35150  neibastop2lem  35240  bj-equsexval  35532  bj-elid3  36043  finxp0  36267  finxp1o  36268  brvdif  37124  xrnss3v  37237  ntrneiel2  42827  ntrneik4w  42841  ismnushort  43050  funressnvmo  45745  dfdfat2  45826