Metamath Proof Explorer

Theorem r19.37

Description: Restricted quantifier version of one direction of 19.37 . (The other direction does not hold when A is empty.) (Contributed by FL, 13-May-2012) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypothesis r19.37.1 x φ
Assertion r19.37 x A φ ψ φ x A ψ


Step Hyp Ref Expression
1 r19.37.1 x φ
2 r19.35 x A φ ψ x A φ x A ψ
3 ax-1 φ x A φ
4 1 3 ralrimi φ x A φ
5 4 imim1i x A φ x A ψ φ x A ψ
6 2 5 sylbi x A φ ψ φ x A ψ