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

Theorem bianabs 542
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 529 . 2 (𝜑 → (𝜒 ↔ (𝜑𝜒)))
31, 2bitr4d 281 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396
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 397
This theorem is referenced by:  ceqsrexv  3643  raltpd  4785  opelopab2a  5535  ov  7551  ovg  7571  soseq  8144  ltprord  11024  isfull  17860  isfth  17864  sltval  27147  axcontlem5  28223  isph  30070  cmbr  30832  cvbr  31530  mdbr  31542  dmdbr  31547  brfldext  32721  brfinext  32727  risc  36849
  Copyright terms: Public domain W3C validator