Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Mixed connectives
orim2
Next ⟩
pm2.38
Metamath Proof Explorer
Ascii
Unicode
Theorem
orim2
Description:
Axiom *1.6 (Sum) of
WhiteheadRussell
p. 97.
(Contributed by
NM
, 3-Jan-2005)
Ref
Expression
Assertion
orim2
⊢
ψ
→
χ
→
φ
∨
ψ
→
φ
∨
χ
Proof
Step
Hyp
Ref
Expression
1
id
⊢
ψ
→
χ
→
ψ
→
χ
2
1
orim2d
⊢
ψ
→
χ
→
φ
∨
ψ
→
φ
∨
χ