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

Theorem bianabs 875
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  3092  raltpd  3997  opelopab2a  4603  ov  6209  ovg  6228  ltprord  9198  isfull  14819  isfth  14823  axcontlem5  23213  isph  24221  cmbr  24986  cvbr  25685  mdbr  25697  dmdbr  25702  soseq  27714  sltval  27787  risc  28790
  Copyright terms: Public domain W3C validator