Metamath Proof Explorer


Theorem 3ori

Description: Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006)

Ref Expression
Hypothesis 3ori.1 φψχ
Assertion 3ori ¬φ¬ψχ

Proof

Step Hyp Ref Expression
1 3ori.1 φψχ
2 ioran ¬φψ¬φ¬ψ
3 df-3or φψχφψχ
4 1 3 mpbi φψχ
5 4 ori ¬φψχ
6 2 5 sylbir ¬φ¬ψχ