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

Theorem bianabs 852
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 492 . 2  |-  ( ph  ->  ( ch  <->  ( ph  /\ 
ch ) ) )
31, 2bitr4d 249 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  ceqsrexv  3070  opelopab2a  4471  ov  6194  ovg  6213  ltprord  8908  isfull  14108  isfth  14112  isph  22324  cmbr  23087  cvbr  23786  mdbr  23798  dmdbr  23803  soseq  25530  sltval  25603  axcontlem5  25908  risc  26603
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 179  df-an 362
  Copyright terms: Public domain W3C validator