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

Theorem bianabs 545
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 532 . 2 (𝜑 → (𝜒 ↔ (𝜑𝜒)))
31, 2bitr4d 285 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  ceqsrexv  3563  raltpd  4697  opelopab2a  5416  ov  7353  ovg  7373  ltprord  10644  isfull  17417  isfth  17421  axcontlem5  27059  isph  28903  cmbr  29665  cvbr  30363  mdbr  30375  dmdbr  30380  brfldext  31436  brfinext  31442  soseq  33540  sltval  33587  risc  35881
  Copyright terms: Public domain W3C validator