Theorem mpbiran2 710

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 709	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  1020  rabtru  3645  reueq  3696  ss0b  4351  eusv1  5329  eusv2nf  5333  eusv2  5334  dfid2  5513  opthprc  5680  sosn  5703  fdmrn  6682  f1cnvcnv  6728  fores  6745  f1orn  6773  funfv  6909  dfoprab2  7404  elxp7  7956  tpostpos  8176  frrlem11  8226  canthwe  10542  opelreal  11021  elreal2  11023  eqresr  11028  elnn1uz2  12823  faclbnd4lem1  14200  isprm2  16593  joindm  18279  meetdm  18293  symgbas0  19302  toptopon  22833  ist1-3  23265  perfcls  23281  prdsxmetlem  24284  eln0s  28288  rusgrprc  29570  hhsssh2  31248  choc0  31304  chocnul  31306  shlesb1i  31364  adjeu  31867  isarchi  33149  derang0  35211  dfon3  35932  brtxpsd  35934  topmeet  36404  filnetlem2  36419  filnetlem3  36420  bj-rabtrALT  36971  bj-snsetex  37003  bj-dfid2ALT  37105  relowlpssretop  37404  poimirlem28  37694  fdc  37791  0totbnd  37819  heiborlem3  37859  cossssid  38510  cnvrefrelcoss2  38580  dfdisjALTV  38757  dfeldisj2  38762  dfeldisj3  38763  dfeldisj4  38764  disjres  38788  disjxrn  38790  dfantisymrel4  38805  dfantisymrel5  38806  antisymrelres  38807  ifpid3g  43531  elintima  43692  brpermmodel  45042  0funcALT  49126