Description: Deduction form of boundvariable hypothesis builder nf3an . (Contributed by NM, 17Feb2013) (Revised by Mario Carneiro, 16Oct2016)
Ref  Expression  

Hypotheses  nfand.1   ( ph > F/ x ps ) 

nfand.2   ( ph > F/ x ch ) 

nfand.3   ( ph > F/ x th ) 

Assertion  nf3and   ( ph > F/ x ( ps /\ ch /\ th ) ) 
Step  Hyp  Ref  Expression 

1  nfand.1   ( ph > F/ x ps ) 

2  nfand.2   ( ph > F/ x ch ) 

3  nfand.3   ( ph > F/ x th ) 

4  df3an   ( ( ps /\ ch /\ th ) <> ( ( ps /\ ch ) /\ th ) ) 

5  1 2  nfand   ( ph > F/ x ( ps /\ ch ) ) 
6  5 3  nfand   ( ph > F/ x ( ( ps /\ ch ) /\ th ) ) 
7  4 6  nfxfrd   ( ph > F/ x ( ps /\ ch /\ th ) ) 