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 524 | . 2 ⊢ (𝜑 → (𝜒 ↔ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | bitr4d 270 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: ceqsrexv 3306 raltpd 4258 opelopab2a 4915 ov 6678 ovg 6697 ltprord 9731 isfull 16393 isfth 16397 axcontlem5 25648 isph 27061 cmbr 27827 cvbr 28525 mdbr 28537 dmdbr 28542 soseq 30995 sltval 31044 risc 32955 |
Copyright terms: Public domain | W3C validator |