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

Theorem bianabs 850
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 490 . 2  |-  ( ph  ->  ( ch  <->  ( ph  /\ 
ch ) ) )
31, 2bitr4d 247 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  ceqsrexv  2914  opelopab2a  4296  ov  5983  ovg  6002  ltprord  8670  isph  21416  cmbr  22179  cvbr  22878  mdbr  22890  dmdbr  22895  soseq  24325  sltval  24372  axcontlem5  24668  risc  26720
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 177  df-an 360
  Copyright terms: Public domain W3C validator