Metamath Proof Explorer

Theorem mpjao3danOLD

Description: Obsolete version of mpjao3dan as of 17-Apr-2024. (Contributed by Thierry Arnoux, 13-Apr-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses mpjao3dan.1 φ ψ χ
mpjao3dan.2 φ θ χ
mpjao3dan.3 φ τ χ
mpjao3dan.4 φ ψ θ τ
Assertion mpjao3danOLD φ χ


Step Hyp Ref Expression
1 mpjao3dan.1 φ ψ χ
2 mpjao3dan.2 φ θ χ
3 mpjao3dan.3 φ τ χ
4 mpjao3dan.4 φ ψ θ τ
5 1 2 jaodan φ ψ θ χ
6 df-3or ψ θ τ ψ θ τ
7 4 6 sylib φ ψ θ τ
8 5 3 7 mpjaodan φ χ