MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbiran2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mpbiran2.1 . 2 𝜒
2 mpbiran2.2 . . 3 (𝜑 ↔ (𝜓𝜒))
32biancomi 463 . 2 (𝜑 ↔ (𝜒𝜓))
41, 3mpbiran 705 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  pm5.62  1012  rabtru  3674  reueq  3725  ss0b  4348  eusv1  5282  eusv2nf  5286  eusv2  5287  opthprc  5609  sosn  5631  fdmrn  6531  f1cnvcnv  6577  fores  6593  f1orn  6618  funfv  6743  dfoprab2  7201  elxp7  7713  tpostpos  7901  canthwe  10061  opelreal  10540  elreal2  10542  eqresr  10547  elnn1uz2  12313  faclbnd4lem1  13641  isprm2  16014  joindm  17601  meetdm  17615  symgbas0  18451  toptopon  21453  ist1-3  21885  perfcls  21901  prdsxmetlem  22905  rusgrprc  27299  hhsssh2  28974  choc0  29030  chocnul  29032  shlesb1i  29090  adjeu  29593  isarchi  30738  derang0  32313  frrlem11  33030  dfon3  33250  brtxpsd  33252  topmeet  33609  filnetlem2  33624  filnetlem3  33625  bj-rabtrALT  34146  bj-snsetex  34172  relowlpssretop  34527  poimirlem28  34801  fdc  34901  0totbnd  34932  heiborlem3  34972  cossssid  35587  cnvrefrelcoss2  35653  dfdisjALTV  35826  dfeldisj2  35831  dfeldisj3  35832  dfeldisj4  35833  disjxrn  35857  ifpid3g  39736  elintima  39876
  Copyright terms: Public domain W3C validator