Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Hankins
Miscellany
exp5d
Next ⟩
exp5g
Metamath Proof Explorer
Ascii
Unicode
Theorem
exp5d
Description:
An exportation inference.
(Contributed by
Jeff Hankins
, 7-Jul-2009)
Ref
Expression
Hypothesis
exp5d.1
⊢
φ
∧
ψ
∧
χ
→
θ
∧
τ
→
η
Assertion
exp5d
⊢
φ
→
ψ
→
χ
→
θ
→
τ
→
η
Proof
Step
Hyp
Ref
Expression
1
exp5d.1
⊢
φ
∧
ψ
∧
χ
→
θ
∧
τ
→
η
2
1
expd
⊢
φ
∧
ψ
∧
χ
→
θ
→
τ
→
η
3
2
exp31
⊢
φ
→
ψ
→
χ
→
θ
→
τ
→
η