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 206  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 207  df-an 396
This theorem is referenced by:  ceqsrexv  3663  raltpd  4806  opelopab2a  5558  ov  7590  ovg  7611  soseq  8196  ltprord  11095  isfull  17972  isfth  17976  sltval  27701  axcontlem5  28992  isph  30845  cmbr  31607  cvbr  32305  mdbr  32317  dmdbr  32322  brfldext  33652  brfinext  33658  risc  37894
  Copyright terms: Public domain W3C validator