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

Theorem bianabs 878
Description: Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)
Hypothesis
Ref Expression
bianabs.1  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ch ) ) )
Assertion
Ref Expression
bianabs  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem bianabs
StepHypRef Expression
1 bianabs.1 . 2  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ch ) ) )
2 ibar 504 . 2  |-  ( ph  ->  ( ch  <->  ( ph  /\ 
ch ) ) )
31, 2bitr4d 256 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> 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:  ceqsrexv  3217  raltpd  4135  opelopab2a  4749  ov  6404  ovg  6423  ltprord  9408  isfull  15150  isfth  15154  axcontlem5  24140  isph  25606  cmbr  26371  cvbr  27070  mdbr  27082  dmdbr  27087  soseq  29306  sltval  29379  risc  30361
  Copyright terms: Public domain W3C validator