theorem nfal {x y: nat} (a: wff x y): $ F/ x a $ > $ F/ x A. y a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax_11 | A. y A. x a -> A. x A. y a |
|
2 | hyp h | F/ x a |
|
3 | 2 | nfi | a -> A. x a |
4 | 3 | alimi | A. y a -> A. y A. x a |
5 | 1, 4 | syl | A. y a -> A. x A. y a |
6 | 5 | nfri | F/ x A. y a |