Theorem nfim 1825

Description: If x is not free in ph and ps, it is not free in ( ph -> ps ). Inference associated with nfimt 1821. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1710 changed. (Revised by Wolf Lammen, 17-Sep-2021.)

Hypotheses

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

Assertion

Ref	Expression
nfim	|- F/ x ( ph -> ps )

Proof of Theorem nfim

Step	Hyp	Ref	Expression
1		nfim.1	. 2 |- F/ x ph
2		nfim.2	. 2 |- F/ x ps
3		nfimt2 1822	. 2 |- ( ( F/ x ph /\ F/ x ps ) -> F/ x ( ph -> ps ) )
4	1, 2, 3	mp2an 708	1 |- F/ x ( ph -> ps )

Syntax hints:   -> wi 4   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfanOLD  1829  nfor  1834  nfia1  2030  nfnf1  2031  nfnf  2158  cbval2  2279  mo2  2479  nfmo1  2481  moexex  2541  cbvralf  3165  vtocl2gf  3268  vtocl3gf  3269  vtoclgaf  3271  vtocl2gaf  3273  vtocl3gaf  3275  rspct  3302  rspc  3303  ralab2  3371  mob  3388  reu2eqd  3403  reu8nf  3516  csbhypf  3552  cbvralcsf  3565  dfss2f  3594  rspn0  3934  elintab  4487  axrep2  4773  axrep3  4774  reusv2lem4  4872  reusv3  4876  iunopeqop  4981  nfpo  5040  nffr  5088  wfisg  5715  fv3  6206  tz6.12c  6213  fvmptss  6292  fvmptd3f  6295  fvmptt  6300  fvmptf  6301  fmptco  6396  dff13f  6513  ovmpt2s  6784  ov2gf  6785  ovmpt2df  6792  ov3  6797  tfis  7054  tfinds  7059  tfindes  7062  findes  7096  dfoprab4f  7226  offval22  7253  tfr3  7495  dom2lem  7995  findcard2  8200  ac6sfi  8204  dfac8clem  8855  aceq1  8940  dfac5lem5  8950  zfcndrep  9436  zfcndinf  9440  pwfseqlem4a  9483  pwfseqlem4  9484  uzind4s  11748  rabssnn0fi  12785  seqof2  12859  rlim2  14227  ello1mpt  14252  o1compt  14318  summolem2a  14446  sumss  14455  fsumsplitf  14472  o1fsum  14545  prodmolem2a  14664  fprodn0  14709  fproddivf  14718  fprodsplitf  14719  fprodsplit1f  14721  prmind2  15398  mreiincl  16256  gsumcom2  18374  gsummptnn0fz  18382  gsummoncoe1  19674  mdetralt2  20415  mdetunilem2  20419  ptcldmpt  21417  cnmptcom  21481  elmptrab  21630  isfildlem  21661  dvmptfsum  23738  dvfsumlem2  23790  dvfsumlem4  23792  dvfsumrlim  23794  dvfsum2  23797  coeeq2  23998  dgrle  23999  rlimcnp  24692  lgamgulmlem2  24756  lgseisenlem2  25101  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  mptelee  25775  gropd  25923  grstructd  25924  isch3  28098  atom1d  29212  vtocl2d  29314  mo5f  29324  ssiun2sf  29378  ssrelf  29425  fmptcof2  29457  aciunf1lem  29462  nn0min  29567  fsumiunle  29575  esum2dlem  30154  fiunelros  30237  measiun  30281  bnj1385  30903  bnj1468  30916  bnj110  30928  bnj849  30995  bnj900  30999  bnj981  31020  bnj1014  31030  bnj1123  31054  bnj1128  31058  bnj1384  31100  bnj1489  31124  bnj1497  31128  setinds  31683  tfisg  31716  frinsg  31742  nosupbnd1  31860  nosupbnd2  31862  subtr  32308  subtr2  32309  bj-cbval2v  32737  bj-axrep2  32789  bj-axrep3  32790  bj-mo3OLD  32832  mptsnunlem  33185  finxpreclem2  33227  finxpreclem6  33233  ptrest  33408  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem28  33437  fdc1  33542  ac6s6  33980  fsumshftd  34237  fsumshftdOLD  34238  cdleme31sn1  35669  cdleme32fva  35725  cdlemk36  36201  fphpd  37380  monotuz  37506  monotoddzz  37508  oddcomabszz  37509  setindtrs  37592  aomclem6  37629  flcidc  37744  rababg  37879  ss2iundf  37951  binomcxplemnotnn0  38555  uzwo4  39221  fiiuncl  39234  disjf1  39369  disjinfi  39380  dmrelrnrel  39419  supxrgere  39549  supxrgelem  39553  supxrge  39554  supxrleubrnmptf  39680  fsumclf  39801  fsummulc1f  39802  fsumnncl  39803  fsumsplit1  39804  fsumf1of  39806  fsumiunss  39807  fsumreclf  39808  fsumlessf  39809  fsumsermpt  39811  fmul01  39812  fmuldfeqlem1  39814  fmuldfeq  39815  fmul01lt1lem1  39816  fmul01lt1lem2  39817  fprodexp  39826  fprodabs2  39827  fprodcnlem  39831  climmulf  39836  climexp  39837  climsuse  39840  climrecf  39841  climinff  39843  climaddf  39847  mullimc  39848  idlimc  39858  neglimc  39879  addlimc  39880  0ellimcdiv  39881  limclner  39883  climsubmpt  39892  climreclf  39896  climeldmeqmpt  39900  climfveqmpt  39903  fnlimfvre  39906  climfveqf  39912  climfveqmpt3  39914  climeldmeqf  39915  limsupref  39917  limsupbnd1f  39918  climeqf  39920  climeldmeqmpt3  39921  climinf2  39939  climinf2mpt  39946  climinfmpt  39947  limsupmnf  39953  limsupequz  39955  limsupre2  39957  limsupequzmptf  39963  limsupre3  39965  cncfshift  40087  cncfiooicclem1  40106  fprodcncf  40114  dvmptmulf  40152  dvnmptdivc  40153  dvnmul  40158  dvmptfprodlem  40159  dvmptfprod  40160  iblspltprt  40189  stoweidlem3  40220  stoweidlem26  40243  stoweidlem31  40248  stoweidlem34  40251  stoweidlem42  40259  stoweidlem43  40260  stoweidlem48  40265  stoweidlem51  40268  stoweidlem59  40276  fourierdlem86  40409  fourierdlem89  40412  fourierdlem91  40414  fourierdlem112  40435  sge0f1o  40599  sge0lempt  40627  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0fodjrnlem  40633  sge0iunmpt  40635  sge0ltfirpmpt2  40643  sge0isummpt2  40649  sge0xaddlem2  40651  sge0xadd  40652  meadjiun  40683  voliunsge0lem  40689  meaiininc  40701  hoimbl2  40879  vonhoire  40886  vonn0ioo2  40904  vonn0icc2  40906  salpreimagelt  40918  salpreimalegt  40920  salpreimagtge  40934  salpreimaltle  40935  salpreimagtlt  40939  2reu4a  41189  eu2ndop1stv  41202  2zrngmmgm  41946  nfsetrecs  42433  setrec2fun  42439