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

Theorem bianabs 541
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 528 . 2 (𝜑 → (𝜒 ↔ (𝜑𝜒)))
31, 2bitr4d 282 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395
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 396
This theorem is referenced by:  ceqsrexv  3639  raltpd  4781  opelopab2a  5531  ov  7559  ovg  7580  soseq  8158  ltprord  11045  isfull  17890  isfth  17894  sltval  27567  axcontlem5  28766  isph  30619  cmbr  31381  cvbr  32079  mdbr  32091  dmdbr  32096  brfldext  33271  brfinext  33277  risc  37394
  Copyright terms: Public domain W3C validator