![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bianbi | Structured version Visualization version GIF version |
Description: Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023.) |
Ref | Expression |
---|---|
bianbi.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
bianbi.2 | ⊢ (𝜓 ↔ 𝜃) |
Ref | Expression |
---|---|
bianbi | ⊢ (𝜑 ↔ (𝜃 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bianbi.1 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | bianbi.2 | . . 3 ⊢ (𝜓 ↔ 𝜃) | |
3 | 2 | anbi1i 623 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜃 ∧ 𝜒)) |
4 | 1, 3 | bitri 275 | 1 ⊢ (𝜑 ↔ (𝜃 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ 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: anbi12i 627 bianassc 642 pm5.53 1005 dfifp4 1067 dfifp5 1068 an3andi 1482 19.28v 1990 19.28 2224 2eu4 2652 r19.26-3 3114 r19.41v 3191 r3ex 3200 3reeanv 3231 r19.41 3264 rmo4 3746 rmo3f 3750 sbc3an 3868 rmo3 3905 difin2 4315 otelxp 5743 dfrefrel5 38421 dfantisymrel4 38665 dfantisymrel5 38666 clnbgrel 47633 grimuhgr 47691 |
Copyright terms: Public domain | W3C validator |