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

Theorem bianabs 545
 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 532 . 2 (𝜑 → (𝜒 ↔ (𝜑𝜒)))
31, 2bitr4d 285 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  ceqsrexv  3598  raltpd  4680  opelopab2a  5391  ov  7284  ovg  7304  ltprord  10459  isfull  17192  isfth  17196  axcontlem5  26806  isph  28649  cmbr  29411  cvbr  30109  mdbr  30121  dmdbr  30126  brfldext  31191  brfinext  31197  soseq  33279  sltval  33337  risc  35575
 Copyright terms: Public domain W3C validator