Metamath Proof Explorer


Theorem 3jaob

Description: Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011) (Proof shortened by Hongxiu Chen, 29-Jun-2025)

Ref Expression
Assertion 3jaob φ χ θ ψ φ ψ χ ψ θ ψ

Proof

Step Hyp Ref Expression
1 pm5.53 φ χ θ ψ φ ψ χ ψ θ ψ
2 df-3or φ χ θ φ χ θ
3 2 imbi1i φ χ θ ψ φ χ θ ψ
4 df-3an φ ψ χ ψ θ ψ φ ψ χ ψ θ ψ
5 1 3 4 3bitr4i φ χ θ ψ φ ψ χ ψ θ ψ