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

Theorem bianabs 960
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 526 . 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  3475  raltpd  4458  opelopab2a  5140  ov  6945  ovg  6964  ltprord  10044  isfull  16771  isfth  16775  axcontlem5  26047  isph  27986  cmbr  28752  cvbr  29450  mdbr  29462  dmdbr  29467  soseq  32060  sltval  32106  risc  34098
  Copyright terms: Public domain W3C validator