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  3609  raltpd  4746  opelopab2a  5496  ov  7503  ovg  7523  soseq  8095  ltprord  10974  isfull  17805  isfth  17809  sltval  27018  axcontlem5  27966  isph  29813  cmbr  30575  cvbr  31273  mdbr  31285  dmdbr  31290  brfldext  32400  brfinext  32406  risc  36495
  Copyright terms: Public domain W3C validator