Metamath Proof Explorer

Theorem 3orbi123

Description: pm4.39 with a 3-conjunct antecedent. This proof is 3orbi123VD automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 3orbi123 φ ψ χ θ τ η φ χ τ ψ θ η


Step Hyp Ref Expression
1 simp1 φ ψ χ θ τ η φ ψ
2 simp2 φ ψ χ θ τ η χ θ
3 simp3 φ ψ χ θ τ η τ η
4 1 2 3 3orbi123d φ ψ χ θ τ η φ χ τ ψ θ η