Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical conjunction
jca32
Next ⟩
jcai
Metamath Proof Explorer
Ascii
Unicode
Theorem
jca32
Description:
Join three consequents.
(Contributed by
FL
, 1-Aug-2009)
Ref
Expression
Hypotheses
jca31.1
⊢
φ
→
ψ
jca31.2
⊢
φ
→
χ
jca31.3
⊢
φ
→
θ
Assertion
jca32
⊢
φ
→
ψ
∧
χ
∧
θ
Proof
Step
Hyp
Ref
Expression
1
jca31.1
⊢
φ
→
ψ
2
jca31.2
⊢
φ
→
χ
3
jca31.3
⊢
φ
→
θ
4
2
3
jca
⊢
φ
→
χ
∧
θ
5
1
4
jca
⊢
φ
→
ψ
∧
χ
∧
θ