Theorem mpbiran2 706

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

Syntax hints:   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  pm5.62  1015  rabtru  3679  reueq  3732  ss0b  4396  eusv1  5388  eusv2nf  5392  eusv2  5393  dfid2  5575  opthprc  5739  sosn  5761  fdmrn  6748  f1cnvcnv  6796  fores  6814  f1orn  6842  funfv  6977  dfoprab2  7469  elxp7  8012  tpostpos  8233  frrlem11  8283  canthwe  10648  opelreal  11127  elreal2  11129  eqresr  11134  elnn1uz2  12913  faclbnd4lem1  14257  isprm2  16623  joindm  18332  meetdm  18346  symgbas0  19297  toptopon  22639  ist1-3  23073  perfcls  23089  prdsxmetlem  24094  rusgrprc  29114  hhsssh2  30790  choc0  30846  chocnul  30848  shlesb1i  30906  adjeu  31409  isarchi  32598  derang0  34458  dfon3  35168  brtxpsd  35170  topmeet  35552  filnetlem2  35567  filnetlem3  35568  bj-rabtrALT  36114  bj-snsetex  36147  bj-dfid2ALT  36249  relowlpssretop  36548  poimirlem28  36819  fdc  36916  0totbnd  36944  heiborlem3  36984  cossssid  37640  cnvrefrelcoss2  37710  dfdisjALTV  37886  dfeldisj2  37891  dfeldisj3  37892  dfeldisj4  37893  disjres  37917  disjxrn  37919  dfantisymrel4  37934  dfantisymrel5  37935  antisymrelres  37936  ifpid3g  42545  elintima  42706