Theorem nfan 1824

Description: If x is not free in ph and ps, it is not free in (ph /\ ps). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortned by Wolf Lammen, 2-Jan-2018.)

Hypotheses

Ref	Expression
nfan.1	|- F/xph
nfan.2	|- F/xps

Assertion

Ref	Expression
nfan	|- F/x(ph /\ ps)

Proof of Theorem nfan

Step	Hyp	Ref	Expression
1		nfan.1	. . . 4 |- F/xph
2	1	a1i 10	. . 3 |- ( T. -> F/xph)
3		nfan.2	. . . 4 |- F/xps
4	3	a1i 10	. . 3 |- ( T. -> F/xps)
5	2, 4	nfand 1822	. 2 |- ( T. -> F/x(ph /\ ps))
6	5	trud 1323	1 |- F/x(ph /\ ps)

Syntax hints:   /\ wa 358   T. wtru 1316   F/wnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by:  nfnan  1825  nf3an  1827  hban  1828  nfbiOLD  1835  nfeqf  1958  nfald2  1972  spimt  1974  dvelimf  1997  cbval2  2004  cbvex2  2005  nfsb4t  2080  dvelimdf  2082  sbcom  2089  nfeud2  2216  mopick  2266  eupicka  2268  mopick2  2271  2eu6  2289  clelab  2474  nfel  2498  nfabd2  2508  2ralbida  2654  ralcom2  2776  reean  2778  cbvreu  2834  cbvrab  2858  ceqsex2  2896  vtocl2gaf  2922  rspce  2951  eqvincf  2968  elrabf  2994  rexab2  3004  morex  3021  reu2  3025  sbc2iegf  3113  rmo2  3132  rmo3  3134  csbiebt  3173  csbie2t  3181  cbvreucsf  3201  cbvrabcsf  3202  eluniab  3904  dfnfc2  3910  iota2  4368  ncfinraise  4482  ncfinlower  4484  nfopd  4606  nfopab  4628  cbvopab  4631  cbvopab1  4633  cbvopab2  4634  cbvopab1s  4635  nfxp  4811  opeliunxp  4821  nfco  4883  nfimad  4955  imadif  5172  nffn  5181  nff  5222  nff1  5257  nffo  5269  nff1o  5286  fun11iun  5306  nffvd  5336  fv3  5342  nfiso  5488  nfoprab  5550  cbvoprab1  5568  cbvoprab2  5569  cbvoprab12  5570  cbvoprab3  5572  mpteq12f  5656  mpt2eq123  5662  nfmpt  5672  nfmpt2  5676  cbvmpt  5677  cbvmpt2x  5679  fmpt2x  5731