Metamath Proof Explorer


Theorem nfifd

Description: Deduction form of nfif . (Contributed by NM, 15-Feb-2013) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypotheses nfifd.2 φxψ
nfifd.3 φ_xA
nfifd.4 φ_xB
Assertion nfifd φ_xifψAB

Proof

Step Hyp Ref Expression
1 nfifd.2 φxψ
2 nfifd.3 φ_xA
3 nfifd.4 φ_xB
4 dfif2 ifψAB=y|yBψyAψ
5 nfv yφ
6 3 nfcrd φxyB
7 6 1 nfimd φxyBψ
8 2 nfcrd φxyA
9 8 1 nfand φxyAψ
10 7 9 nfimd φxyBψyAψ
11 5 10 nfabdw φ_xy|yBψyAψ
12 4 11 nfcxfrd φ_xifψAB