Theorem mpbiran2 716

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm5.62  1026  rabtru  3634  reueq  3685  ss0b  4336  eusv1  5327  eusv2nf  5331  eusv2  5332  dfid2  5522  opthprc  5689  sosn  5712  fdmrn  6693  f1cnvcnv  6739  fores  6756  f1orn  6784  funfv  6921  dfoprab2  7421  elxp7  7973  tpostpos  8193  frrlem11  8243  canthwe  10572  opelreal  11051  elreal2  11053  eqresr  11058  elnn1uz2  12873  faclbnd4lem1  14253  isprm2  16649  joindm  18337  meetdm  18351  symgbas0  19362  toptopon  22907  ist1-3  23339  perfcls  23355  prdsxmetlem  24358  eln0s  28378  rusgrprc  29684  hhsssh2  31366  choc0  31422  chocnul  31424  shlesb1i  31482  adjeu  31985  isarchi  33270  derang0  35404  dfon3  36125  brtxpsd  36127  topmeet  36599  filnetlem2  36614  filnetlem3  36615  bj-rabtrALT  37291  bj-snsetex  37323  bj-dfid2ALT  37425  relowlpssretop  37733  poimirlem28  38022  fdc  38119  0totbnd  38147  heiborlem3  38187  cossssid  38931  cnvrefrelcoss2  38991  dfdisjALTV  39172  dfeldisj2  39184  dfeldisj3  39185  dfeldisj4  39186  disjqmap2  39200  disjres  39218  disjxrn  39220  dfantisymrel4  39238  dfantisymrel5  39239  antisymrelres  39240  ifpid3g  43943  elintima  44104  brpermmodel  45454  0funcALT  49585