Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter II Implication
rp-7frege
Next ⟩
rp-4frege
Metamath Proof Explorer
Ascii
Unicode
Theorem
rp-7frege
Description:
Distribute antecedent and add another.
(Contributed by
RP
, 24-Dec-2019)
Ref
Expression
Assertion
rp-7frege
⊢
φ
→
ψ
→
χ
→
θ
→
φ
→
ψ
→
φ
→
χ
Proof
Step
Hyp
Ref
Expression
1
ax-frege2
⊢
φ
→
ψ
→
χ
→
φ
→
ψ
→
φ
→
χ
2
rp-frege24
⊢
φ
→
ψ
→
χ
→
φ
→
ψ
→
φ
→
χ
→
φ
→
ψ
→
χ
→
θ
→
φ
→
ψ
→
φ
→
χ
3
1
2
ax-mp
⊢
φ
→
ψ
→
χ
→
θ
→
φ
→
ψ
→
φ
→
χ