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