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

Theorem bianabs 923
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 525 . 2 (𝜑 → (𝜒 ↔ (𝜑𝜒)))
31, 2bitr4d 271 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  ceqsrexv  3319  raltpd  4285  opelopab2a  4950  ov  6733  ovg  6752  ltprord  9796  isfull  16491  isfth  16495  axcontlem5  25748  isph  27523  cmbr  28289  cvbr  28987  mdbr  28999  dmdbr  29004  soseq  31449  sltval  31498  risc  33414
  Copyright terms: Public domain W3C validator