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 461 . 2 (𝜑 ↔ (𝜒𝜓))
41, 3mpbiran 705 1 (𝜑𝜓)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator