Mathbox for Jonathan Ben-Naim |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj252 | Structured version Visualization version GIF version |
Description: ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
Ref | Expression |
---|---|
bnj252 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj250 30020 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) | |
2 | df-3an 1033 | . . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃)) | |
3 | 2 | anbi2i 726 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) |
4 | 1, 3 | bitr4i 266 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 ∧ w3a 1031 ∧ w-bnj17 30005 |
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 df-3an 1033 df-bnj17 30006 |
This theorem is referenced by: bnj290 30029 bnj563 30067 bnj919 30091 bnj976 30102 bnj543 30217 bnj570 30229 bnj594 30236 bnj916 30257 bnj917 30258 bnj964 30267 bnj983 30275 bnj984 30276 bnj998 30280 bnj999 30281 bnj1021 30288 bnj1083 30300 bnj1450 30372 |
Copyright terms: Public domain | W3C validator |