Theorem nfan 1614

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 shortened by Wolf Lammen, 13-Jan-2018.)

Hypotheses

Ref	Expression
nfan.1	|- F/ x ph
nfan.2	|- F/ x ps

Assertion

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

Proof of Theorem nfan

Step	Hyp	Ref	Expression
1		nfan.1	. 2 |- F/ x ph
2		nfan.2	. . 3 |- F/ x ps
3	2	a1i 9	. 2 |- ( ph -> F/ x ps )
4	1, 3	nfan1 1613	1 |- F/ x ( ph /\ ps )

Syntax hints:   /\ wa 104   F/wnf 1509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559

This theorem depends on definitions:  df-bi 117  df-nf 1510

This theorem is referenced by:  nf3an  1615  cbvex2  1971  nfsbxyt  1996  nfsbv  2000  sbcomxyyz  2025  nfsb4t  2067  clelab  2358  nfel  2384  2ralbida  2554  r19.29an  2676  reean  2703  nfrabw  2715  cbvrmow  2717  cbvrexfw  2758  cbvrexf  2760  cbvreu  2766  cbvrab  2801  ceqsex2  2845  vtocl2gaf  2872  rspce  2906  eqvincf  2932  elrabf  2961  elrab3t  2962  rexab2  2973  morex  2991  reu2  2995  rmo3f  3004  sbc2iegf  3103  reu8nf  3114  rmo2ilem  3123  rmo3  3125  csbiebt  3168  csbie2t  3177  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  rabsnifsb  3741  nfopd  3884  eluniab  3910  dfnfc2  3916  nfdisjv  4081  disjiun  4088  nfopab  4162  cbvopab  4165  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  mpteq12f  4174  nfmpt  4186  cbvmptf  4188  cbvmpt  4189  repizf2  4258  nfpo  4404  nfso  4405  nfwe  4458  onintonm  4621  peano2  4699  nfxp  4758  opeliunxp  4787  nfco  4901  elrnmpt1  4989  nfimad  5091  iota2  5323  dffun4f  5349  nffun  5356  imadif  5417  funimaexglem  5420  nffn  5433  nff  5486  nff1  5549  nffo  5567  nff1o  5590  fun11iun  5613  nffvd  5660  fv3  5671  fmptco  5821  nfiso  5957  cbvriota  5993  riota2df  6003  riota5f  6008  nfoprab  6083  mpoeq123  6090  nfmpo  6100  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvoprab3  6107  cbvmpox  6109  ovmpodxf  6157  elovmporab  6232  elovmporab1w  6233  opabex3d  6292  opabex3  6293  uchoice  6309  dfoprab4f  6365  fmpox  6374  spc2ed  6407  cnvoprab  6408  f1od2  6409  opeliunxp2f  6447  nfrecs  6516  tfri3  6576  nffrec  6605  erovlem  6839  nfixpxy  6929  nfixp1  6930  modom  7037  xpf1o  7073  nneneq  7086  ac6sfi  7130  opabfi  7175  nfsup  7234  exmidomni  7384  fodjuomnilemdc  7386  ismkvnex  7397  mkvprop  7400  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  cc3  7530  caucvgsrlemgt1  8058  suplocsrlem  8071  axpre-suploclemres  8164  supinfneg  9873  infsupneg  9874  zsupcllemstep  10535  nninfinf  10751  reuccatpfxs1  11377  fimaxre2  11850  nfsum1  11979  nfsum  11980  fsumsplitf  12032  fsum2dlemstep  12058  fsum00  12086  nfcprod1  12178  nfcprod  12179  prodeq2  12181  fprod2dlemstep  12246  fprodsplitf  12256  fprodsplit1f  12258  fprodap0f  12260  fprodle  12264  bezoutlemmain  12632  bezoutlemzz  12636  bezout  12645  exmidunben  13110  ctiunctlemfo  13123  ctiunct  13124  mulcncf  15402  ellimc3apf  15454  limccnp2cntop  15471  bdsepnft  16586  bdsepnfALT  16588  bj-findis  16678  strcollnft  16683  strcollnfALT  16685  pw1nct  16708  isomninnlem  16745  trirec0  16759  iswomninnlem  16765  ismkvnnlem  16768