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  3645  reueq  3697  ss0b  4352  eusv1  5330  eusv2nf  5334  eusv2  5335  dfid2  5516  opthprc  5683  sosn  5706  fdmrn  6683  f1cnvcnv  6729  fores  6746  f1orn  6774  funfv  6910  dfoprab2  7407  elxp7  7959  tpostpos  8179  frrlem11  8229  canthwe  10545  opelreal  11024  elreal2  11026  eqresr  11031  elnn1uz2  12826  faclbnd4lem1  14200  isprm2  16593  joindm  18279  meetdm  18293  symgbas0  19268  toptopon  22802  ist1-3  23234  perfcls  23250  prdsxmetlem  24254  eln0s  28258  rusgrprc  29540  hhsssh2  31218  choc0  31274  chocnul  31276  shlesb1i  31334  adjeu  31837  isarchi  33133  derang0  35162  dfon3  35886  brtxpsd  35888  topmeet  36358  filnetlem2  36373  filnetlem3  36374  bj-rabtrALT  36925  bj-snsetex  36957  bj-dfid2ALT  37059  relowlpssretop  37358  poimirlem28  37648  fdc  37745  0totbnd  37773  heiborlem3  37813  cossssid  38464  cnvrefrelcoss2  38534  dfdisjALTV  38711  dfeldisj2  38716  dfeldisj3  38717  dfeldisj4  38718  disjres  38742  disjxrn  38744  dfantisymrel4  38759  dfantisymrel5  38760  antisymrelres  38761  ifpid3g  43485  elintima  43646  brpermmodel  44997  0funcALT  49093