![]() |
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 530 | . 2 ⊢ (𝜑 → (𝜒 ↔ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | bitr4d 282 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 |
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 398 |
This theorem is referenced by: ceqsrexv 3644 raltpd 4786 opelopab2a 5536 ov 7552 ovg 7572 soseq 8145 ltprord 11025 isfull 17861 isfth 17865 sltval 27150 axcontlem5 28257 isph 30106 cmbr 30868 cvbr 31566 mdbr 31578 dmdbr 31583 brfldext 32757 brfinext 32763 risc 36902 |
Copyright terms: Public domain | W3C validator |