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 31966 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) | |
2 | df-3an 1085 | . . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃)) | |
3 | 2 | anbi2i 624 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) |
4 | 1, 3 | bitr4i 280 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∧ w3a 1083 ∧ w-bnj17 31951 |
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 df-3an 1085 df-bnj17 31952 |
This theorem is referenced by: bnj290 31975 bnj563 32009 bnj919 32033 bnj976 32044 bnj543 32160 bnj570 32172 bnj594 32179 bnj916 32200 bnj917 32201 bnj964 32210 bnj983 32218 bnj984 32219 bnj998 32224 bnj999 32225 bnj1021 32233 bnj1083 32245 bnj1450 32317 |
Copyright terms: Public domain | W3C validator |