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

Theorem bianabs 880
Description: Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)
Hypothesis
Ref Expression
bianabs.1
Assertion
Ref Expression
bianabs

Proof of Theorem bianabs
StepHypRef Expression
1 bianabs.1 . 2
2 ibar 504 . 2
31, 2bitr4d 256 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  ceqsrexv  3233  raltpd  4153  opelopab2a  4767  ov  6422  ovg  6441  ltprord  9429  isfull  15279  isfth  15283  axcontlem5  24271  isph  25737  cmbr  26502  cvbr  27201  mdbr  27213  dmdbr  27218  soseq  29334  sltval  29407  risc  30389
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
  Copyright terms: Public domain W3C validator