Metamath Proof Explorer


Theorem 19.3t

Description: Closed form of 19.3 and version of 19.9t with a universal quantifier. (Contributed by NM, 9-Nov-2020) (Proof shortened by BJ, 9-Oct-2022)

Ref Expression
Assertion 19.3t x φ x φ φ

Proof

Step Hyp Ref Expression
1 sp x φ φ
2 nf5r x φ φ x φ
3 1 2 impbid2 x φ x φ φ