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  3692  reueq  3746  ss0b  4407  eusv1  5397  eusv2nf  5401  eusv2  5402  dfid2  5585  opthprc  5753  sosn  5775  fdmrn  6768  f1cnvcnv  6814  fores  6831  f1orn  6859  funfv  6996  dfoprab2  7491  elxp7  8048  tpostpos  8270  frrlem11  8320  canthwe  10689  opelreal  11168  elreal2  11170  eqresr  11175  elnn1uz2  12965  faclbnd4lem1  14329  isprm2  16716  joindm  18433  meetdm  18447  symgbas0  19421  toptopon  22939  ist1-3  23373  perfcls  23389  prdsxmetlem  24394  eln0s  28373  rusgrprc  29623  hhsssh2  31299  choc0  31355  chocnul  31357  shlesb1i  31415  adjeu  31918  isarchi  33172  derang0  35154  dfon3  35874  brtxpsd  35876  topmeet  36347  filnetlem2  36362  filnetlem3  36363  bj-rabtrALT  36914  bj-snsetex  36946  bj-dfid2ALT  37048  relowlpssretop  37347  poimirlem28  37635  fdc  37732  0totbnd  37760  heiborlem3  37800  cossssid  38449  cnvrefrelcoss2  38519  dfdisjALTV  38695  dfeldisj2  38700  dfeldisj3  38701  dfeldisj4  38702  disjres  38726  disjxrn  38728  dfantisymrel4  38743  dfantisymrel5  38744  antisymrelres  38745  ifpid3g  43482  elintima  43643