Theorem mpbiran2 722

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 401

This theorem is referenced by:  pm5.62  1034  rabtru  3651  reueq  3703  ss0b  4358  eusv1  5353  eusv2nf  5357  eusv2  5358  dfid2  5549  opthprc  5716  sosn  5739  fdmrn  6727  f1cnvcnv  6775  fores  6792  f1orn  6821  funfv  6958  dfoprab2  7458  elxp7  8009  tpostpos  8230  frrlem11  8281  canthwe  10624  opelreal  11103  elreal2  11105  eqresr  11110  elnn1uz2  12940  faclbnd4lem1  14320  isprm2  16730  joindm  18419  meetdm  18433  symgbas0  19450  toptopon  23035  ist1-3  23467  perfcls  23483  prdsxmetlem  24486  eln0s  28512  rusgrprc  29849  hhsssh2  31531  choc0  31587  chocnul  31589  shlesb1i  31647  adjeu  32150  isarchi  33415  vonf1osev  35467  derang0  35532  dfon3  36253  brtxpsd  36255  topmeet  36737  filnetlem2  36752  filnetlem3  36753  bj-rabtrALT  37428  bj-snsetex  37460  bj-dfid2ALT  37562  relowlpssretop  37870  poimirlem28  38159  fdc  38256  0totbnd  38284  heiborlem3  38324  cossssid  39068  cnvrefrelcoss2  39128  dfdisjALTV  39309  dfeldisj2  39321  dfeldisj3  39322  dfeldisj4  39323  disjqmap2  39337  disjres  39355  disjxrn  39357  dfantisymrel4  39375  dfantisymrel5  39376  antisymrelres  39377  ifpid3g  44080  elintima  44241  brpermmodel  45577  0funcALT  49717