Metamath Proof Explorer


Theorem orfa1

Description: Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017)

Ref Expression
Hypothesis orfa1.1 φ ψ
Assertion orfa1 φ ψ

Proof

Step Hyp Ref Expression
1 orfa1.1 φ ψ
2 falim ψ
3 1 2 jaoi φ ψ