Metamath Proof Explorer

Theorem nfia1

Description: Lemma 23 of Monk2 p. 114. (Contributed by Mario Carneiro, 24-Sep-2016)

Ref Expression
Assertion nfia1 
|- F/ x ( A. x ph -> A. x ps )

Proof

Step Hyp Ref Expression
1 nfa1 
 |-  F/ x A. x ph
2 nfa1 
 |-  F/ x A. x ps
3 1 2 nfim 
 |-  F/ x ( A. x ph -> A. x ps )