New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > an4 | GIF version |
Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.) |
Ref | Expression |
---|---|
an4 | ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ ((φ ∧ χ) ∧ (ψ ∧ θ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an12 772 | . . 3 ⊢ ((ψ ∧ (χ ∧ θ)) ↔ (χ ∧ (ψ ∧ θ))) | |
2 | 1 | anbi2i 675 | . 2 ⊢ ((φ ∧ (ψ ∧ (χ ∧ θ))) ↔ (φ ∧ (χ ∧ (ψ ∧ θ)))) |
3 | anass 630 | . 2 ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ (φ ∧ (ψ ∧ (χ ∧ θ)))) | |
4 | anass 630 | . 2 ⊢ (((φ ∧ χ) ∧ (ψ ∧ θ)) ↔ (φ ∧ (χ ∧ (ψ ∧ θ)))) | |
5 | 2, 3, 4 | 3bitr4i 268 | 1 ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ ((φ ∧ χ) ∧ (ψ ∧ θ))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 ∧ wa 358 |
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 177 df-an 360 |
This theorem is referenced by: an42 798 an4s 799 anandi 801 anandir 802 rnlem 931 an6 1261 2eu1 2284 2eu4 2287 reean 2777 reu2 3024 rmo4 3029 rmo3 3133 inxpk 4277 dfpw12 4301 ltfintr 4459 opelxp 4811 inxp 4863 xp11 5056 fununi 5160 2elresin 5194 fun 5236 resoprab2 5582 brtxp 5783 qrpprod 5836 fundmen 6043 |
Copyright terms: Public domain | W3C validator |