Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical disjunction
pm1.4
Next ⟩
orcom
Metamath Proof Explorer
Ascii
Unicode
Theorem
pm1.4
Description:
Axiom *1.4 of
WhiteheadRussell
p. 96.
(Contributed by
NM
, 3-Jan-2005)
Ref
Expression
Assertion
pm1.4
⊢
φ
∨
ψ
→
ψ
∨
φ
Proof
Step
Hyp
Ref
Expression
1
olc
⊢
φ
→
ψ
∨
φ
2
orc
⊢
ψ
→
ψ
∨
φ
3
1
2
jaoi
⊢
φ
∨
ψ
→
ψ
∨
φ