Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
dalemclqjt
Next ⟩
dalemclrju
Metamath Proof Explorer
Ascii
Unicode
Theorem
dalemclqjt
Description:
Lemma for
dath
. Frequently-used utility lemma.
(Contributed by
NM
, 13-Aug-2012)
Ref
Expression
Hypothesis
dalema.ph
⊢
φ
↔
K
∈
HL
∧
C
∈
Base
K
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
Y
∈
O
∧
Z
∈
O
∧
¬
C
≤
˙
P
∨
˙
Q
∧
¬
C
≤
˙
Q
∨
˙
R
∧
¬
C
≤
˙
R
∨
˙
P
∧
¬
C
≤
˙
S
∨
˙
T
∧
¬
C
≤
˙
T
∨
˙
U
∧
¬
C
≤
˙
U
∨
˙
S
∧
C
≤
˙
P
∨
˙
S
∧
C
≤
˙
Q
∨
˙
T
∧
C
≤
˙
R
∨
˙
U
Assertion
dalemclqjt
⊢
φ
→
C
≤
˙
Q
∨
˙
T
Proof
Step
Hyp
Ref
Expression
1
dalema.ph
⊢
φ
↔
K
∈
HL
∧
C
∈
Base
K
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
Y
∈
O
∧
Z
∈
O
∧
¬
C
≤
˙
P
∨
˙
Q
∧
¬
C
≤
˙
Q
∨
˙
R
∧
¬
C
≤
˙
R
∨
˙
P
∧
¬
C
≤
˙
S
∨
˙
T
∧
¬
C
≤
˙
T
∨
˙
U
∧
¬
C
≤
˙
U
∨
˙
S
∧
C
≤
˙
P
∨
˙
S
∧
C
≤
˙
Q
∨
˙
T
∧
C
≤
˙
R
∨
˙
U
2
simp332
⊢
K
∈
HL
∧
C
∈
Base
K
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
Y
∈
O
∧
Z
∈
O
∧
¬
C
≤
˙
P
∨
˙
Q
∧
¬
C
≤
˙
Q
∨
˙
R
∧
¬
C
≤
˙
R
∨
˙
P
∧
¬
C
≤
˙
S
∨
˙
T
∧
¬
C
≤
˙
T
∨
˙
U
∧
¬
C
≤
˙
U
∨
˙
S
∧
C
≤
˙
P
∨
˙
S
∧
C
≤
˙
Q
∨
˙
T
∧
C
≤
˙
R
∨
˙
U
→
C
≤
˙
Q
∨
˙
T
3
1
2
sylbi
⊢
φ
→
C
≤
˙
Q
∨
˙
T