Theorem mpbiran2 723

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm5.62  1036  rabtru  3643  reueq  3695  ss0b  4351  eusv1  5353  eusv2nf  5357  eusv2  5358  dfid2  5548  opthprc  5715  sosn  5738  fdmrn  6733  f1cnvcnv  6781  fores  6798  f1orn  6827  funfv  6964  dfoprab2  7470  elxp7  8025  tpostpos  8247  frrlem11  8298  canthwe  10717  opelreal  11196  elreal2  11198  eqresr  11203  elnn1uz2  13033  faclbnd4lem1  14417  isprm2  16837  joindm  18527  meetdm  18541  symgbas0  19583  toptopon  23215  ist1-3  23647  perfcls  23663  prdsxmetlem  24667  eln0s  28729  rusgrprc  30153  hhsssh2  31854  choc0  31910  chocnul  31912  shlesb1i  31970  adjeu  32473  isarchi  33725  vonf1osev  35864  derang0  35903  dfon3  36624  brtxpsd  36626  topmeet  37122  filnetlem2  37137  filnetlem3  37138  bj-rabtrALT  37814  bj-snsetex  37846  bj-dfid2ALT  37948  relowlpssretop  38255  poimirlem28  38534  fdc  38647  0totbnd  38675  heiborlem3  38715  cossssid  39457  cnvrefrelcoss2  39517  dfdisjALTV  39698  dfeldisj2  39710  dfeldisj3  39711  dfeldisj4  39712  disjqmap2  39726  disjres  39744  disjxrn  39746  dfantisymrel4  39764  dfantisymrel5  39765  antisymrelres  39766  ifpid3g  44451  elintima  44612  brpermmodel  45945  0funcALT  50140