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

Theorem mpbiran2 927
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)
Hypotheses
Ref Expression
mpbiran2.1  |-  ch
mpbiran2.2  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
mpbiran2  |-  ( ph  <->  ps )

Proof of Theorem mpbiran2
StepHypRef Expression
1 mpbiran2.2 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
2 mpbiran2.1 . . 3  |-  ch
32biantru 507 . 2  |-  ( ps  <->  ( ps  /\  ch )
)
41, 3bitr4i 255 1  |-  ( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm5.62  931  reueq  3268  ss0b  3794  eusv1  4618  eusv2nf  4622  eusv2  4623  opthprc  4901  sosn  4923  opelres  5129  fdmrn  5761  f1cnvcnv  5804  fores  5819  f1orn  5841  funfv  5948  dfoprab2  6351  elxp7  6840  tpostpos  7004  canthwe  9083  recmulnq  9396  opelreal  9561  elreal2  9563  eqresr  9568  elnn1uz2  11242  faclbnd4lem1  12484  isprm2  14631  joindm  16248  meetdm  16262  symgbas0  17034  efgs1  17384  toptopon  19946  ist1-3  20363  perfcls  20379  prdsxmetlem  21381  hhsssh2  26919  choc0  26977  chocnul  26979  shlesb1i  27037  adjeu  27540  isarchi  28506  derang0  29900  nofulllem5  30600  brtxp  30652  brpprod  30657  dfon3  30664  brtxpsd  30666  topmeet  31025  filnetlem2  31040  filnetlem3  31041  bj-rabtrALT  31503  bj-snsetex  31525  relowlpssretop  31731  poimirlem28  31932  fdc  32038  0totbnd  32069  heiborlem3  32109  ifpid3g  36106  elintima  36215
  Copyright terms: Public domain W3C validator