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 φψχζ