Theorem mpbiran2 709

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 708	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  1019  rabtru  3705  reueq  3759  ss0b  4424  eusv1  5409  eusv2nf  5413  eusv2  5414  dfid2  5595  opthprc  5764  sosn  5786  fdmrn  6779  f1cnvcnv  6826  fores  6844  f1orn  6872  funfv  7009  dfoprab2  7508  elxp7  8065  tpostpos  8287  frrlem11  8337  canthwe  10720  opelreal  11199  elreal2  11201  eqresr  11206  elnn1uz2  12990  faclbnd4lem1  14342  isprm2  16729  joindm  18445  meetdm  18459  symgbas0  19430  toptopon  22944  ist1-3  23378  perfcls  23394  prdsxmetlem  24399  eln0s  28376  rusgrprc  29626  hhsssh2  31302  choc0  31358  chocnul  31360  shlesb1i  31418  adjeu  31921  isarchi  33162  derang0  35137  dfon3  35856  brtxpsd  35858  topmeet  36330  filnetlem2  36345  filnetlem3  36346  bj-rabtrALT  36897  bj-snsetex  36929  bj-dfid2ALT  37031  relowlpssretop  37330  poimirlem28  37608  fdc  37705  0totbnd  37733  heiborlem3  37773  cossssid  38423  cnvrefrelcoss2  38493  dfdisjALTV  38669  dfeldisj2  38674  dfeldisj3  38675  dfeldisj4  38676  disjres  38700  disjxrn  38702  dfantisymrel4  38717  dfantisymrel5  38718  antisymrelres  38719  ifpid3g  43454  elintima  43615