This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfim1

Description: A closed form of nfim . (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 2-Jan-2018) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021)

Ref Expression
Hypotheses nfim1.1 
|- F/ x ph
nfim1.2 
|- ( ph -> F/ x ps )
Assertion nfim1 
|- F/ x ( ph -> ps )

Proof

Step Hyp Ref Expression
1 nfim1.1 
 |-  F/ x ph
2 nfim1.2 
 |-  ( ph -> F/ x ps )
3 nf3 
 |-  ( F/ x ph <-> ( A. x ph \/ A. x -. ph ) )
4 1 3 mpbi 
 |-  ( A. x ph \/ A. x -. ph )
5 nftht 
 |-  ( A. x ph -> F/ x ph )
6 2 sps 
 |-  ( A. x ph -> F/ x ps )
7 5 6 nfimd 
 |-  ( A. x ph -> F/ x ( ph -> ps ) )
8 pm2.21 
 |-  ( -. ph -> ( ph -> ps ) )
9 8 alimi 
 |-  ( A. x -. ph -> A. x ( ph -> ps ) )
10 nftht 
 |-  ( A. x ( ph -> ps ) -> F/ x ( ph -> ps ) )
11 9 10 syl 
 |-  ( A. x -. ph -> F/ x ( ph -> ps ) )
12 7 11 jaoi 
 |-  ( ( A. x ph \/ A. x -. ph ) -> F/ x ( ph -> ps ) )
13 4 12 ax-mp 
 |-  F/ x ( ph -> ps )