Theorem mpbiran2 720

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 466	. 2 ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))
4	1, 3	mpbiran 719	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  pm5.62  1031  rabtru  3648  reueq  3699  ss0b  4354  eusv1  5347  eusv2nf  5351  eusv2  5352  dfid2  5542  opthprc  5709  sosn  5732  fdmrn  6719  f1cnvcnv  6767  fores  6784  f1orn  6813  funfv  6950  dfoprab2  7450  elxp7  8001  tpostpos  8221  frrlem11  8272  canthwe  10606  opelreal  11085  elreal2  11087  eqresr  11092  elnn1uz2  12923  faclbnd4lem1  14303  isprm2  16699  joindm  18388  meetdm  18402  symgbas0  19412  toptopon  22957  ist1-3  23389  perfcls  23405  prdsxmetlem  24408  eln0s  28431  rusgrprc  29737  hhsssh2  31419  choc0  31475  chocnul  31477  shlesb1i  31535  adjeu  32038  isarchi  33323  vonf1osev  35419  derang0  35483  dfon3  36204  brtxpsd  36206  topmeet  36688  filnetlem2  36703  filnetlem3  36704  bj-rabtrALT  37380  bj-snsetex  37412  bj-dfid2ALT  37514  relowlpssretop  37822  poimirlem28  38111  fdc  38208  0totbnd  38236  heiborlem3  38276  cossssid  39020  cnvrefrelcoss2  39080  dfdisjALTV  39261  dfeldisj2  39273  dfeldisj3  39274  dfeldisj4  39275  disjqmap2  39289  disjres  39307  disjxrn  39309  dfantisymrel4  39327  dfantisymrel5  39328  antisymrelres  39329  ifpid3g  44032  elintima  44193  brpermmodel  45543  0funcALT  49673