Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical disjunction
pm2.32
Next ⟩
pm2.3
Metamath Proof Explorer
Ascii
Unicode
Theorem
pm2.32
Description:
Theorem *2.32 of
WhiteheadRussell
p. 105.
(Contributed by
NM
, 3-Jan-2005)
Ref
Expression
Assertion
pm2.32
⊢
φ
∨
ψ
∨
χ
→
φ
∨
ψ
∨
χ
Proof
Step
Hyp
Ref
Expression
1
orass
⊢
φ
∨
ψ
∨
χ
↔
φ
∨
ψ
∨
χ
2
1
biimpi
⊢
φ
∨
ψ
∨
χ
→
φ
∨
ψ
∨
χ