Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Zhi Wang
Topology
Separated spaces: T0, T1, T2 (Hausdorff) ...
iscnrm3lem3
Next ⟩
iscnrm3lem4
Metamath Proof Explorer
Ascii
Unicode
Theorem
iscnrm3lem3
Description:
Lemma for
iscnrm3lem4
.
(Contributed by
Zhi Wang
, 4-Sep-2024)
Ref
Expression
Assertion
iscnrm3lem3
⊢
φ
∧
ψ
∧
χ
∧
θ
↔
φ
∧
χ
∧
θ
∧
ψ
Proof
Step
Hyp
Ref
Expression
1
anass
⊢
φ
∧
ψ
∧
χ
∧
θ
↔
φ
∧
ψ
∧
χ
∧
θ
2
anass
⊢
φ
∧
χ
∧
θ
∧
ψ
↔
φ
∧
χ
∧
θ
∧
ψ
3
3anass
⊢
φ
∧
χ
∧
θ
↔
φ
∧
χ
∧
θ
4
3
anbi1i
⊢
φ
∧
χ
∧
θ
∧
ψ
↔
φ
∧
χ
∧
θ
∧
ψ
5
ancom
⊢
ψ
∧
χ
∧
θ
↔
χ
∧
θ
∧
ψ
6
5
anbi2i
⊢
φ
∧
ψ
∧
χ
∧
θ
↔
φ
∧
χ
∧
θ
∧
ψ
7
2
4
6
3bitr4ri
⊢
φ
∧
ψ
∧
χ
∧
θ
↔
φ
∧
χ
∧
θ
∧
ψ
8
1
7
bitri
⊢
φ
∧
ψ
∧
χ
∧
θ
↔
φ
∧
χ
∧
θ
∧
ψ