Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Stanislas Polu
IMO Problems
IMO 1972 B2
syldbl2
Next ⟩
suprlubrd
Metamath Proof Explorer
Ascii
Unicode
Theorem
syldbl2
Description:
Stacked hypotheseis implies goal.
(Contributed by
Stanislas Polu
, 9-Mar-2020)
Ref
Expression
Hypothesis
syldbl2.1
⊢
φ
∧
ψ
→
ψ
→
θ
Assertion
syldbl2
⊢
φ
∧
ψ
→
θ
Proof
Step
Hyp
Ref
Expression
1
syldbl2.1
⊢
φ
∧
ψ
→
ψ
→
θ
2
1
com12
⊢
ψ
→
φ
∧
ψ
→
θ
3
2
anabsi7
⊢
φ
∧
ψ
→
θ