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

Syntax hints:   ↔ wb 209   ∧ 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 210  df-an 400

This theorem is referenced by:  pm5.62  1016  rabtru  3625  reueq  3676  ss0b  4305  eusv1  5257  eusv2nf  5261  eusv2  5262  opthprc  5580  sosn  5602  fdmrn  6512  f1cnvcnv  6559  fores  6575  f1orn  6600  funfv  6725  dfoprab2  7191  elxp7  7706  tpostpos  7895  canthwe  10062  opelreal  10541  elreal2  10543  eqresr  10548  elnn1uz2  12313  faclbnd4lem1  13649  isprm2  16016  joindm  17605  meetdm  17619  symgbas0  18509  toptopon  21522  ist1-3  21954  perfcls  21970  prdsxmetlem  22975  rusgrprc  27380  hhsssh2  29053  choc0  29109  chocnul  29111  shlesb1i  29169  adjeu  29672  isarchi  30861  derang0  32529  frrlem11  33246  dfon3  33466  brtxpsd  33468  topmeet  33825  filnetlem2  33840  filnetlem3  33841  bj-rabtrALT  34373  bj-snsetex  34399  relowlpssretop  34781  poimirlem28  35085  fdc  35183  0totbnd  35211  heiborlem3  35251  cossssid  35867  cnvrefrelcoss2  35933  dfdisjALTV  36106  dfeldisj2  36111  dfeldisj3  36112  dfeldisj4  36113  disjxrn  36137  ifpid3g  40200  elintima  40354