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

Theorem mpbiran2 917
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 505 . 2  |-  ( ps  <->  ( ps  /\  ch )
)
41, 3bitr4i 252 1  |-  ( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  pm5.62  921  reueq  3301  ss0b  3815  eusv1  4641  eusv2nf  4645  eusv2  4646  opthprc  5046  sosn  5068  opelres  5277  fdmrn  5744  f1cnvcnv  5787  fores  5802  f1orn  5824  funfv  5932  dfoprab2  6325  elxp7  6814  tpostpos  6972  dfsup2OLD  7899  canthwe  9025  recmulnq  9338  opelreal  9503  elreal2  9505  eqresr  9510  elnn1uz2  11154  faclbnd4lem1  12335  isprm2  14080  joindm  15486  meetdm  15500  symgbas0  16214  efgs1  16549  funsnfsupOLD  18027  toptopon  19201  ist1-3  19616  perfcls  19632  prdsxmetlem  20606  hhsssh2  25862  choc0  25920  chocnul  25922  shlesb1i  25980  adjeu  26484  isarchi  27388  derang0  28253  nofulllem5  29043  brtxp  29107  brpprod  29112  dfon3  29119  brtxpsd  29121  topmeet  29785  filnetlem2  29800  filnetlem3  29801  fdc  29841  0totbnd  29872  heiborlem3  29912  bj-rabtrALT  33579  bj-snsetex  33602
  Copyright terms: Public domain W3C validator