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

Theorem bianabs 920
 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 524 . 2 (𝜑 → (𝜒 ↔ (𝜑𝜒)))
31, 2bitr4d 270 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385 This theorem is referenced by:  ceqsrexv  3306  raltpd  4258  opelopab2a  4915  ov  6678  ovg  6697  ltprord  9731  isfull  16393  isfth  16397  axcontlem5  25648  isph  27061  cmbr  27827  cvbr  28525  mdbr  28537  dmdbr  28542  soseq  30995  sltval  31044  risc  32955
 Copyright terms: Public domain W3C validator