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

Theorem bianabs 942
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 271 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  ceqsrexv  3367  raltpd  4346  opelopab2a  5019  ov  6822  ovg  6841  ltprord  9890  isfull  16617  isfth  16621  axcontlem5  25893  isph  27805  cmbr  28571  cvbr  29269  mdbr  29281  dmdbr  29286  soseq  31879  sltval  31925  risc  33915
  Copyright terms: Public domain W3C validator