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