Theorem mpbiran2 710

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 709	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  1020  rabtru  3659  reueq  3711  ss0b  4367  eusv1  5349  eusv2nf  5353  eusv2  5354  dfid2  5538  opthprc  5705  sosn  5728  fdmrn  6722  f1cnvcnv  6768  fores  6785  f1orn  6813  funfv  6951  dfoprab2  7450  elxp7  8006  tpostpos  8228  frrlem11  8278  canthwe  10611  opelreal  11090  elreal2  11092  eqresr  11097  elnn1uz2  12891  faclbnd4lem1  14265  isprm2  16659  joindm  18341  meetdm  18355  symgbas0  19326  toptopon  22811  ist1-3  23243  perfcls  23259  prdsxmetlem  24263  eln0s  28258  rusgrprc  29525  hhsssh2  31206  choc0  31262  chocnul  31264  shlesb1i  31322  adjeu  31825  isarchi  33143  derang0  35163  dfon3  35887  brtxpsd  35889  topmeet  36359  filnetlem2  36374  filnetlem3  36375  bj-rabtrALT  36926  bj-snsetex  36958  bj-dfid2ALT  37060  relowlpssretop  37359  poimirlem28  37649  fdc  37746  0totbnd  37774  heiborlem3  37814  cossssid  38465  cnvrefrelcoss2  38535  dfdisjALTV  38712  dfeldisj2  38717  dfeldisj3  38718  dfeldisj4  38719  disjres  38743  disjxrn  38745  dfantisymrel4  38760  dfantisymrel5  38761  antisymrelres  38762  ifpid3g  43488  elintima  43649  brpermmodel  45000  0funcALT  49081