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  3642  reueq  3694  ss0b  4350  eusv1  5352  eusv2nf  5356  eusv2  5357  dfid2  5547  opthprc  5714  sosn  5737  fdmrn  6741  f1cnvcnv  6789  fores  6806  f1orn  6835  funfv  6972  dfoprab2  7478  elxp7  8036  tpostpos  8266  frrlem11  8317  canthwe  10739  opelreal  11218  elreal2  11220  eqresr  11225  elnn1uz2  13055  faclbnd4lem1  14440  isprm2  16862  joindm  18552  meetdm  18566  symgbas0  19608  toptopon  23240  ist1-3  23672  perfcls  23688  prdsxmetlem  24692  eln0s  28752  rusgrprc  30176  hhsssh2  31877  choc0  31933  chocnul  31935  shlesb1i  31993  adjeu  32496  isarchi  33789  vonf1osev  35959  derang0  36020  dfon3  36746  brtxpsd  36748  topmeet  37244  filnetlem2  37259  filnetlem3  37260  bj-rabtrALT  37936  bj-snsetex  37968  bj-dfid2ALT  38072  relowlpssretop  38380  poimirlem28  38659  fdc  38772  0totbnd  38800  heiborlem3  38840  cossssid  39582  cnvrefrelcoss2  39642  dfdisjALTV  39823  dfeldisj2  39835  dfeldisj3  39836  dfeldisj4  39837  disjqmap2  39851  disjres  39869  disjxrn  39871  dfantisymrel4  39889  dfantisymrel5  39890  antisymrelres  39891  ifpid3g  44586  elintima  44746  brpermmodel  46086  0funcALT  50296