![]() |
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 528 | . 2 ⊢ (𝜑 → (𝜒 ↔ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | bitr4d 282 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
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 207 df-an 396 |
This theorem is referenced by: ceqsrexv 3668 raltpd 4806 opelopab2a 5554 ov 7594 ovg 7615 soseq 8200 ltprord 11099 isfull 17977 isfth 17981 sltval 27710 axcontlem5 29001 isph 30854 cmbr 31616 cvbr 32314 mdbr 32326 dmdbr 32331 brfldext 33660 brfinext 33666 risc 37946 |
Copyright terms: Public domain | W3C validator |