|   | 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 34715 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) | |
| 2 | df-3an 1089 | . . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃)) | |
| 3 | 2 | anbi2i 623 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) | 
| 4 | 1, 3 | bitr4i 278 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∧ w3a 1087 ∧ w-bnj17 34700 | 
| 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 df-3an 1089 df-bnj17 34701 | 
| This theorem is referenced by: bnj290 34724 bnj563 34757 bnj919 34781 bnj976 34791 bnj543 34907 bnj570 34919 bnj594 34926 bnj916 34947 bnj917 34948 bnj964 34957 bnj983 34965 bnj984 34966 bnj998 34971 bnj999 34972 bnj1021 34980 bnj1083 34992 bnj1450 35064 | 
| Copyright terms: Public domain | W3C validator |