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  3656  reueq  3708  ss0b  4364  eusv1  5346  eusv2nf  5350  eusv2  5351  dfid2  5535  opthprc  5702  sosn  5725  fdmrn  6719  f1cnvcnv  6765  fores  6782  f1orn  6810  funfv  6948  dfoprab2  7447  elxp7  8003  tpostpos  8225  frrlem11  8275  canthwe  10604  opelreal  11083  elreal2  11085  eqresr  11090  elnn1uz2  12884  faclbnd4lem1  14258  isprm2  16652  joindm  18334  meetdm  18348  symgbas0  19319  toptopon  22804  ist1-3  23236  perfcls  23252  prdsxmetlem  24256  eln0s  28251  rusgrprc  29518  hhsssh2  31199  choc0  31255  chocnul  31257  shlesb1i  31315  adjeu  31818  isarchi  33136  derang0  35156  dfon3  35880  brtxpsd  35882  topmeet  36352  filnetlem2  36367  filnetlem3  36368  bj-rabtrALT  36919  bj-snsetex  36951  bj-dfid2ALT  37053  relowlpssretop  37352  poimirlem28  37642  fdc  37739  0totbnd  37767  heiborlem3  37807  cossssid  38458  cnvrefrelcoss2  38528  dfdisjALTV  38705  dfeldisj2  38710  dfeldisj3  38711  dfeldisj4  38712  disjres  38736  disjxrn  38738  dfantisymrel4  38753  dfantisymrel5  38754  antisymrelres  38755  ifpid3g  43481  elintima  43642  brpermmodel  44993  0funcALT  49077