Theorem mpbiran2 706

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm5.62  1013  rabtru  3615  reueq  3662  ss0b  4271  eusv1  5183  eusv2nf  5187  eusv2  5188  opthprc  5502  sosn  5524  fdmrn  6406  f1cnvcnv  6452  fores  6468  f1orn  6493  funfv  6617  dfoprab2  7071  elxp7  7580  tpostpos  7763  canthwe  9919  opelreal  10398  elreal2  10400  eqresr  10405  elnn1uz2  12174  faclbnd4lem1  13503  isprm2  15855  joindm  17442  meetdm  17456  symgbas0  18253  toptopon  21209  ist1-3  21641  perfcls  21657  prdsxmetlem  22661  rusgrprc  27055  hhsssh2  28738  choc0  28794  chocnul  28796  shlesb1i  28854  adjeu  29357  isarchi  30449  derang0  32025  frrlem11  32743  dfon3  32963  brtxpsd  32965  topmeet  33322  filnetlem2  33337  filnetlem3  33338  bj-rabtrALT  33824  bj-snsetex  33899  relowlpssretop  34195  poimirlem28  34470  fdc  34571  0totbnd  34602  heiborlem3  34642  cossssid  35257  cnvrefrelcoss2  35323  dfdisjALTV  35496  dfeldisj2  35501  dfeldisj3  35502  dfeldisj4  35503  disjxrn  35527  ifpid3g  39362  elintima  39502