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  3668  raltpd  4806  opelopab2a  5554  ov  7594  ovg  7615  soseq  8200  ltprord  11099  isfull  17977  isfth  17981  sltval  27710  axcontlem5  29001  isph  30854  cmbr  31616  cvbr  32314  mdbr  32326  dmdbr  32331  brfldext  33660  brfinext  33666  risc  37946
  Copyright terms: Public domain W3C validator