Metamath Proof Explorer


Theorem 3jaoi

Description: Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995)

Ref Expression
Hypotheses 3jaoi.1 φψ
3jaoi.2 χψ
3jaoi.3 θψ
Assertion 3jaoi φχθψ

Proof

Step Hyp Ref Expression
1 3jaoi.1 φψ
2 3jaoi.2 χψ
3 3jaoi.3 θψ
4 1 2 3 3pm3.2i φψχψθψ
5 3jao φψχψθψφχθψ
6 4 5 ax-mp φχθψ