Theorem mpbiran2 722

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)

Hypotheses

Ref	Expression
mpbiran2.1	⊢ 𝜒
mpbiran2.2	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
mpbiran2	⊢ (𝜑 ↔ 𝜓)

Proof of Theorem mpbiran2

Step	Hyp	Ref	Expression
1		mpbiran2.1	. 2 ⊢ 𝜒
2		mpbiran2.2	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3	2	biancomi 467	. 2 ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))
4	1, 3	mpbiran 721	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  pm5.62  1036  rabtru  3649  reueq  3701  ss0b  4359  eusv1  5364  eusv2nf  5368  eusv2  5369  dfid2  5560  opthprc  5727  sosn  5750  fdmrn  6739  f1cnvcnv  6787  fores  6804  f1orn  6833  funfv  6970  dfoprab2  7470  elxp7  8022  tpostpos  8243  frrlem11  8294  canthwe  10637  opelreal  11116  elreal2  11118  eqresr  11123  elnn1uz2  12950  faclbnd4lem1  14331  isprm2  16741  joindm  18430  meetdm  18444  symgbas0  19460  toptopon  23055  ist1-3  23487  perfcls  23503  prdsxmetlem  24506  eln0s  28532  rusgrprc  29918  hhsssh2  31600  choc0  31656  chocnul  31658  shlesb1i  31716  adjeu  32219  isarchi  33480  vonf1osev  35574  derang0  35639  dfon3  36360  brtxpsd  36362  topmeet  36853  filnetlem2  36868  filnetlem3  36869  bj-rabtrALT  37545  bj-snsetex  37577  bj-dfid2ALT  37679  relowlpssretop  37988  poimirlem28  38277  fdc  38374  0totbnd  38402  heiborlem3  38442  cossssid  39184  cnvrefrelcoss2  39244  dfdisjALTV  39425  dfeldisj2  39437  dfeldisj3  39438  dfeldisj4  39439  disjqmap2  39453  disjres  39471  disjxrn  39473  dfantisymrel4  39491  dfantisymrel5  39492  antisymrelres  39493  ifpid3g  44198  elintima  44359  brpermmodel  45692  0funcALT  49843