Theorem mpbiran2 711

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 710	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  1021  rabtru  3646  reueq  3697  ss0b  4355  eusv1  5338  eusv2nf  5342  eusv2  5343  dfid2  5529  opthprc  5696  sosn  5719  fdmrn  6701  f1cnvcnv  6747  fores  6764  f1orn  6792  funfv  6929  dfoprab2  7426  elxp7  7978  tpostpos  8198  frrlem11  8248  canthwe  10574  opelreal  11053  elreal2  11055  eqresr  11060  elnn1uz2  12850  faclbnd4lem1  14228  isprm2  16621  joindm  18308  meetdm  18322  symgbas0  19330  toptopon  22873  ist1-3  23305  perfcls  23321  prdsxmetlem  24324  eln0s  28369  rusgrprc  29676  hhsssh2  31357  choc0  31413  chocnul  31415  shlesb1i  31473  adjeu  31976  isarchi  33275  derang0  35382  dfon3  36103  brtxpsd  36105  topmeet  36577  filnetlem2  36592  filnetlem3  36593  bj-rabtrALT  37173  bj-snsetex  37205  bj-dfid2ALT  37307  relowlpssretop  37613  poimirlem28  37893  fdc  37990  0totbnd  38018  heiborlem3  38058  cossssid  38802  cnvrefrelcoss2  38862  dfdisjALTV  39043  dfeldisj2  39055  dfeldisj3  39056  dfeldisj4  39057  disjqmap2  39071  disjres  39089  disjxrn  39091  dfantisymrel4  39109  dfantisymrel5  39110  antisymrelres  39111  ifpid3g  43842  elintima  44003  brpermmodel  45353  0funcALT  49441