Metamath Proof Explorer


Theorem 3jaodd

Description: Double deduction form of 3jaoi . (Contributed by Scott Fenton, 20-Apr-2011)

Ref Expression
Hypotheses 3jaodd.1 φ ψ χ η
3jaodd.2 φ ψ θ η
3jaodd.3 φ ψ τ η
Assertion 3jaodd φ ψ χ θ τ η

Proof

Step Hyp Ref Expression
1 3jaodd.1 φ ψ χ η
2 3jaodd.2 φ ψ θ η
3 3jaodd.3 φ ψ τ η
4 1 com3r χ φ ψ η
5 2 com3r θ φ ψ η
6 3 com3r τ φ ψ η
7 4 5 6 3jaoi χ θ τ φ ψ η
8 7 com3l φ ψ χ θ τ η