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 283 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  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 208  df-an 397
This theorem is referenced by:  ceqsrexv  3587  raltpd  4623  opelopab2a  5312  ov  7150  ovg  7169  ltprord  10298  isfull  17009  isfth  17013  axcontlem5  26437  isph  28290  cmbr  29052  cvbr  29750  mdbr  29762  dmdbr  29767  brfldext  30641  brfinext  30647  soseq  32705  sltval  32763  risc  34796
  Copyright terms: Public domain W3C validator