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  3242  raltpd  4156  opelopab2a  4768  ov  6417  ovg  6436  ltprord  9420  isfull  15154  isfth  15158  axcontlem5  24094  isph  25560  cmbr  26325  cvbr  27024  mdbr  27036  dmdbr  27041  soseq  29261  sltval  29334  risc  30316
  Copyright terms: Public domain W3C validator