![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bianabs | Structured version Visualization version GIF version |
Description: Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.) |
Ref | Expression |
---|---|
bianabs.1 | ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜒))) |
Ref | Expression |
---|---|
bianabs | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bianabs.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜒))) | |
2 | ibar 529 | . 2 ⊢ (𝜑 → (𝜒 ↔ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | bitr4d 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 |