Metamath Proof Explorer

Theorem stdpc5t

Description: Closed form of stdpc5 . (Possible to place it before 19.21t and use it to prove 19.21t ). (Contributed by BJ, 15-Sep-2018) (Proof modification is discouraged.)

Ref Expression
Assertion stdpc5t x φ x φ ψ φ x ψ


Step Hyp Ref Expression
1 nf5r x φ φ x φ
2 alim x φ ψ x φ x ψ
3 1 2 syl9 x φ x φ ψ φ x ψ