Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical disjunction
imori
Next ⟩
imorri
Metamath Proof Explorer
Ascii
Unicode
Theorem
imori
Description:
Infer disjunction from implication.
(Contributed by
NM
, 12-Mar-2012)
Ref
Expression
Hypothesis
imori.1
⊢
φ
→
ψ
Assertion
imori
⊢
¬
φ
∨
ψ
Proof
Step
Hyp
Ref
Expression
1
imori.1
⊢
φ
→
ψ
2
imor
⊢
φ
→
ψ
↔
¬
φ
∨
ψ
3
1
2
mpbi
⊢
¬
φ
∨
ψ