Metamath Proof Explorer


Theorem ee01an

Description: e01an without virtual deductions. sylancr is also a form of e01an without virtual deduction, except the order of the hypotheses is different. (Contributed by Alan Sare, 25-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ee01an.1 φ
ee01an.2 ψ χ
ee01an.3 φ χ θ
Assertion ee01an ψ θ

Proof

Step Hyp Ref Expression
1 ee01an.1 φ
2 ee01an.2 ψ χ
3 ee01an.3 φ χ θ
4 1 2 3 sylancr ψ θ