Theorem mpbiran2 710

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 462	. 2 ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))
4	1, 3	mpbiran 709	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:  pm5.62  1020  rabtru  3673  reueq  3725  ss0b  4381  eusv1  5366  eusv2nf  5370  eusv2  5371  dfid2  5555  opthprc  5723  sosn  5746  fdmrn  6742  f1cnvcnv  6788  fores  6805  f1orn  6833  funfv  6971  dfoprab2  7470  elxp7  8028  tpostpos  8250  frrlem11  8300  canthwe  10670  opelreal  11149  elreal2  11151  eqresr  11156  elnn1uz2  12946  faclbnd4lem1  14316  isprm2  16706  joindm  18390  meetdm  18404  symgbas0  19375  toptopon  22860  ist1-3  23292  perfcls  23308  prdsxmetlem  24312  eln0s  28308  rusgrprc  29575  hhsssh2  31256  choc0  31312  chocnul  31314  shlesb1i  31372  adjeu  31875  isarchi  33185  derang0  35196  dfon3  35915  brtxpsd  35917  topmeet  36387  filnetlem2  36402  filnetlem3  36403  bj-rabtrALT  36954  bj-snsetex  36986  bj-dfid2ALT  37088  relowlpssretop  37387  poimirlem28  37677  fdc  37774  0totbnd  37802  heiborlem3  37842  cossssid  38490  cnvrefrelcoss2  38560  dfdisjALTV  38736  dfeldisj2  38741  dfeldisj3  38742  dfeldisj4  38743  disjres  38767  disjxrn  38769  dfantisymrel4  38784  dfantisymrel5  38785  antisymrelres  38786  ifpid3g  43483  elintima  43644  brpermmodel  44995  0funcALT  49020