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

Theorem mpbiran2 956
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.2 . 2 (𝜑 ↔ (𝜓𝜒))
2 mpbiran2.1 . . 3 𝜒
32biantru 525 . 2 (𝜓 ↔ (𝜓𝜒))
41, 3bitr4i 266 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  pm5.62  960  reueq  3371  ss0b  3925  eusv1  4786  eusv2nf  4790  eusv2  4791  opthprc  5089  sosn  5111  opelres  5322  fdmrn  5977  f1cnvcnv  6022  fores  6037  f1orn  6060  funfv  6175  dfoprab2  6599  elxp7  7092  tpostpos  7259  canthwe  9352  recmulnq  9665  opelreal  9830  elreal2  9832  eqresr  9837  elnn1uz2  11641  faclbnd4lem1  12942  isprm2  15233  joindm  16826  meetdm  16840  symgbas0  17637  efgs1  17971  toptopon  20548  ist1-3  20963  perfcls  20979  prdsxmetlem  21983  hhsssh2  27511  choc0  27569  chocnul  27571  shlesb1i  27629  adjeu  28132  isarchi  29067  derang0  30405  nofulllem5  31105  brtxp  31157  brpprod  31162  dfon3  31169  brtxpsd  31171  topmeet  31529  filnetlem2  31544  filnetlem3  31545  bj-rabtrALT  32119  bj-snsetex  32144  relowlpssretop  32388  poimirlem28  32607  fdc  32711  0totbnd  32742  heiborlem3  32782  ifpid3g  36856  elintima  36964  rusgrprc  40790
  Copyright terms: Public domain W3C validator