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

Theorem bianabs 543
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 530 . 2 (𝜑 → (𝜒 ↔ (𝜑𝜒)))
31, 2bitr4d 282 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  ceqsrexv  3644  raltpd  4786  opelopab2a  5536  ov  7552  ovg  7572  soseq  8145  ltprord  11025  isfull  17861  isfth  17865  sltval  27150  axcontlem5  28257  isph  30106  cmbr  30868  cvbr  31566  mdbr  31578  dmdbr  31583  brfldext  32757  brfinext  32763  risc  36902
  Copyright terms: Public domain W3C validator