Theorem mpbiran2 709

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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  pm5.62  1018  rabtru  3641  reueq  3694  ss0b  4356  eusv1  5345  eusv2nf  5349  eusv2  5350  dfid2  5531  opthprc  5693  sosn  5715  fdmrn  6696  f1cnvcnv  6744  fores  6762  f1orn  6790  funfv  6924  dfoprab2  7408  elxp7  7947  tpostpos  8145  frrlem11  8195  canthwe  10521  opelreal  11000  elreal2  11002  eqresr  11007  elnn1uz2  12780  faclbnd4lem1  14122  isprm2  16494  joindm  18200  meetdm  18214  symgbas0  19105  toptopon  22194  ist1-3  22628  perfcls  22644  prdsxmetlem  23649  rusgrprc  28343  hhsssh2  30017  choc0  30073  chocnul  30075  shlesb1i  30133  adjeu  30636  isarchi  31819  derang0  33543  dfon3  34408  brtxpsd  34410  topmeet  34767  filnetlem2  34782  filnetlem3  34783  bj-rabtrALT  35332  bj-snsetex  35365  bj-dfid2ALT  35467  relowlpssretop  35766  poimirlem28  36037  fdc  36135  0totbnd  36163  heiborlem3  36203  cossssid  36860  cnvrefrelcoss2  36930  dfdisjALTV  37106  dfeldisj2  37111  dfeldisj3  37112  dfeldisj4  37113  disjres  37137  disjxrn  37139  dfantisymrel4  37154  dfantisymrel5  37155  antisymrelres  37156  ifpid3g  41563  elintima  41724