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  3633  reueq  3684  ss0b  4342  eusv1  5328  eusv2nf  5332  eusv2  5333  dfid2  5521  opthprc  5688  sosn  5711  fdmrn  6693  f1cnvcnv  6739  fores  6756  f1orn  6784  funfv  6921  dfoprab2  7418  elxp7  7970  tpostpos  8189  frrlem11  8239  canthwe  10565  opelreal  11044  elreal2  11046  eqresr  11051  elnn1uz2  12866  faclbnd4lem1  14246  isprm2  16642  joindm  18330  meetdm  18344  symgbas0  19355  toptopon  22892  ist1-3  23324  perfcls  23340  prdsxmetlem  24343  eln0s  28367  rusgrprc  29674  hhsssh2  31356  choc0  31412  chocnul  31414  shlesb1i  31472  adjeu  31975  isarchi  33258  derang0  35367  dfon3  36088  brtxpsd  36090  topmeet  36562  filnetlem2  36577  filnetlem3  36578  bj-rabtrALT  37254  bj-snsetex  37286  bj-dfid2ALT  37388  relowlpssretop  37694  poimirlem28  37983  fdc  38080  0totbnd  38108  heiborlem3  38148  cossssid  38892  cnvrefrelcoss2  38952  dfdisjALTV  39133  dfeldisj2  39145  dfeldisj3  39146  dfeldisj4  39147  disjqmap2  39161  disjres  39179  disjxrn  39181  dfantisymrel4  39199  dfantisymrel5  39200  antisymrelres  39201  ifpid3g  43937  elintima  44098  brpermmodel  45448  0funcALT  49575