Metamath Proof Explorer


Theorem ee323

Description: e323 without virtual deductions. (Contributed by Alan Sare, 17-Apr-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ee323.1 φ ψ χ θ
ee323.2 φ ψ τ
ee323.3 φ ψ χ η
ee323.4 θ τ η ζ
Assertion ee323 φ ψ χ ζ

Proof

Step Hyp Ref Expression
1 ee323.1 φ ψ χ θ
2 ee323.2 φ ψ τ
3 ee323.3 φ ψ χ η
4 ee323.4 θ τ η ζ
5 2 a1dd φ ψ χ τ
6 1 5 3 4 ee333 φ ψ χ ζ