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  3632  reueq  3683  ss0b  4341  eusv1  5333  eusv2nf  5337  eusv2  5338  dfid2  5528  opthprc  5695  sosn  5718  fdmrn  6699  f1cnvcnv  6745  fores  6762  f1orn  6790  funfv  6927  dfoprab2  7425  elxp7  7977  tpostpos  8196  frrlem11  8246  canthwe  10574  opelreal  11053  elreal2  11055  eqresr  11060  elnn1uz2  12875  faclbnd4lem1  14255  isprm2  16651  joindm  18339  meetdm  18353  symgbas0  19364  toptopon  22882  ist1-3  23314  perfcls  23330  prdsxmetlem  24333  eln0s  28353  rusgrprc  29659  hhsssh2  31341  choc0  31397  chocnul  31399  shlesb1i  31457  adjeu  31960  isarchi  33243  derang0  35351  dfon3  36072  brtxpsd  36074  topmeet  36546  filnetlem2  36561  filnetlem3  36562  bj-rabtrALT  37238  bj-snsetex  37270  bj-dfid2ALT  37372  relowlpssretop  37680  poimirlem28  37969  fdc  38066  0totbnd  38094  heiborlem3  38134  cossssid  38878  cnvrefrelcoss2  38938  dfdisjALTV  39119  dfeldisj2  39131  dfeldisj3  39132  dfeldisj4  39133  disjqmap2  39147  disjres  39165  disjxrn  39167  dfantisymrel4  39185  dfantisymrel5  39186  antisymrelres  39187  ifpid3g  43919  elintima  44080  brpermmodel  45430  0funcALT  49563