Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Hankins
Miscellany
imp5q
Next ⟩
ecase13d
Metamath Proof Explorer
Ascii
Unicode
Theorem
imp5q
Description:
A triple importation inference.
(Contributed by
Jeff Hankins
, 8-Jul-2009)
Ref
Expression
Hypothesis
3imp5.1
⊢
φ
→
ψ
→
χ
→
θ
→
τ
→
η
Assertion
imp5q
⊢
φ
∧
ψ
→
χ
∧
θ
∧
τ
→
η
Proof
Step
Hyp
Ref
Expression
1
3imp5.1
⊢
φ
→
ψ
→
χ
→
θ
→
τ
→
η
2
1
imp
⊢
φ
∧
ψ
→
χ
→
θ
→
τ
→
η
3
2
3impd
⊢
φ
∧
ψ
→
χ
∧
θ
∧
τ
→
η