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