Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Abbreviated conjunction and disjunction of three wff's
3impd
Next ⟩
3imp2
Metamath Proof Explorer
Ascii
Unicode
Theorem
3impd
Description:
Importation deduction for triple conjunction.
(Contributed by
NM
, 26-Oct-2006)
Ref
Expression
Hypothesis
3imp1.1
⊢
φ
→
ψ
→
χ
→
θ
→
τ
Assertion
3impd
⊢
φ
→
ψ
∧
χ
∧
θ
→
τ
Proof
Step
Hyp
Ref
Expression
1
3imp1.1
⊢
φ
→
ψ
→
χ
→
θ
→
τ
2
1
com4l
⊢
ψ
→
χ
→
θ
→
φ
→
τ
3
2
3imp
⊢
ψ
∧
χ
∧
θ
→
φ
→
τ
4
3
com12
⊢
φ
→
ψ
∧
χ
∧
θ
→
τ