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 531 | . 2 ⊢ (𝜑 → (𝜒 ↔ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | bitr4d 284 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: ceqsrexv 3648 raltpd 4709 opelopab2a 5414 ov 7288 ovg 7307 ltprord 10446 isfull 17174 isfth 17178 axcontlem5 26748 isph 28593 cmbr 29355 cvbr 30053 mdbr 30065 dmdbr 30070 brfldext 31032 brfinext 31038 soseq 33091 sltval 33149 risc 35258 |
Copyright terms: Public domain | W3C validator |