Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical conjunction
syldbl2
Next ⟩
mpsyl4anc
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
⊢
φ
∧
ψ
→
θ