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

Theorem bianabs 542
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 529 . 2 (𝜑 → (𝜒 ↔ (𝜑𝜒)))
31, 2bitr4d 281 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396
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 206  df-an 397
This theorem is referenced by:  ceqsrexv  3605  raltpd  4742  opelopab2a  5492  ov  7498  ovg  7518  soseq  8090  ltprord  10965  isfull  17796  isfth  17800  sltval  26993  axcontlem5  27915  isph  29762  cmbr  30524  cvbr  31222  mdbr  31234  dmdbr  31239  brfldext  32327  brfinext  32333  risc  36436
  Copyright terms: Public domain W3C validator