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

Theorem bianabs 537
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 524 . 2 (𝜑 → (𝜒 ↔ (𝜑𝜒)))
31, 2bitr4d 273 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  ceqsrexv  3489  raltpd  4468  opelopab2a  5151  ov  6978  ovg  6997  ltprord  10105  isfull  16837  isfth  16841  axcontlem5  26139  isph  28068  cmbr  28834  cvbr  29532  mdbr  29544  dmdbr  29549  soseq  32130  sltval  32176  risc  34139
  Copyright terms: Public domain W3C validator