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

Theorem mpbiran2 886
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 492 . 2  |-  ( ps  <->  ( ps  /\  ch )
)
41, 3bitr4i 244 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  pm5.62  890  reueq  3099  ss0b  3625  eusv1  4684  eusv2nf  4688  eusv2  4689  opthprc  4892  sosn  4914  opelres  5118  f1cnvcnv  5614  fores  5629  f1orn  5651  funfv  5757  dfoprab2  6088  elxp7  6346  tpostpos  6466  dfsup2OLD  7414  canthwe  8490  recmulnq  8805  opelreal  8969  elreal2  8971  eqresr  8976  elnn1uz2  10516  faclbnd4lem1  11547  isprm2  13050  efgs1  15330  toptopon  16961  ist1-3  17375  perfcls  17391  prdsxmetlem  18359  hhsssh2  22731  choc0  22789  chocnul  22791  shlesb1i  22849  adjeu  23353  fdmrn  24000  isarchi  24213  derang0  24816  nofulllem5  25582  brtxp  25642  brpprod  25647  dfon3  25654  brtxpsd  25656  topmeet  26291  filnetlem2  26306  filnetlem3  26307  fdc  26347  0totbnd  26380  heiborlem3  26420  funsnfsup  26641
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator