![]() |
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 33712 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) | |
2 | df-3an 1090 | . . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃)) | |
3 | 2 | anbi2i 624 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) |
4 | 1, 3 | bitr4i 278 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∧ w3a 1088 ∧ w-bnj17 33697 |
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 206 df-an 398 df-3an 1090 df-bnj17 33698 |
This theorem is referenced by: bnj290 33721 bnj563 33754 bnj919 33778 bnj976 33788 bnj543 33904 bnj570 33916 bnj594 33923 bnj916 33944 bnj917 33945 bnj964 33954 bnj983 33962 bnj984 33963 bnj998 33968 bnj999 33969 bnj1021 33977 bnj1083 33989 bnj1450 34061 |
Copyright terms: Public domain | W3C validator |