Metamath Proof Explorer

Theorem 19.23bi

Description: Inference form of Theorem 19.23 of Margaris p. 90, see 19.23 . (Contributed by NM, 12-Mar-1993)

Ref Expression
Hypothesis 19.23bi.1 x φ ψ
Assertion 19.23bi φ ψ


Step Hyp Ref Expression
1 19.23bi.1 x φ ψ
2 19.8a φ x φ
3 2 1 syl φ ψ