Theorem nfim 1893

Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 → 𝜓). Inference associated with nfimt 1892. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1781 changed. (Revised by Wolf Lammen, 17-Sep-2021.)

Hypotheses

Ref	Expression
nfim.1	⊢ Ⅎ𝑥𝜑
nfim.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfim	⊢ Ⅎ𝑥(𝜑 → 𝜓)

Proof of Theorem nfim

Step	Hyp	Ref	Expression
1		nfim.1	. 2 ⊢ Ⅎ𝑥𝜑
2		nfim.2	. 2 ⊢ Ⅎ𝑥𝜓
3		nfimt 1892	. 2 ⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓))
4	1, 2, 3	mp2an 690	1 ⊢ Ⅎ𝑥(𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1780

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfor  1901  nfia1  2153  nfnf1  2154  nfnf  2341  nfsbv  2345  nfsbvOLD  2346  cbval2vOLD  2360  cbval2OLD  2429  mof  2643  moexexlem  2707  nfabdw  3000  cbvralfw  3437  cbvralf  3439  vtocl2gf  3569  vtocl3gf  3570  vtoclgaf  3572  vtocl2gaf  3575  vtocl3gaf  3576  rspct  3608  rspc  3610  ralab2  3687  ralab2OLD  3688  mob  3707  reu2eqd  3726  reu8nf  3859  csbhypf  3910  cbvralcsf  3924  vtocl2dOLD  3930  dfss2f  3957  rspn0  4312  2reu4lem  4464  reusngf  4605  rexreusng  4610  reuprg0  4631  elintab  4879  axrep2  5185  axrep3  5186  reusv2lem4  5293  reusv3  5297  iunopeqop  5403  nfpo  5473  nffr  5523  reuop  6138  wfisg  6177  fv3  6682  fvmptss  6774  fvmptd3f  6777  fvmptt  6782  fvmptf  6783  fmptco  6885  dff13f  7008  ovmpos  7292  ov2gf  7293  ovmpodf  7300  ov3  7305  tfis  7563  tfinds  7568  tfindes  7571  findes  7606  dfoprab4f  7748  offval22  7777  tfr3  8029  dom2lem  8543  findcard2  8752  ac6sfi  8756  dfac8clem  9452  aceq1  9537  dfac5lem5  9547  zfcndrep  10030  zfcndinf  10034  pwfseqlem4a  10077  pwfseqlem4  10078  uzind4s  12302  rabssnn0fi  13348  seqof2  13422  rlim2  14847  ello1mpt  14872  o1compt  14938  summolem2a  15066  sumss  15075  fsumsplitf  15092  o1fsum  15162  prodmolem2a  15282  fprodn0  15327  fproddivf  15335  fprodsplitf  15336  fprodsplit1f  15338  prmind2  16023  mreiincl  16861  gsumcom2  19089  gsummptnn0fz  19100  gsummoncoe1  20466  mdetralt2  21212  mdetunilem2  21216  ptcldmpt  22216  cnmptcom  22280  elmptrab  22429  isfildlem  22459  dvmptfsum  24566  dvfsumlem2  24618  dvfsumlem4  24620  dvfsumrlim  24622  dvfsum2  24625  coeeq2  24826  dgrle  24827  rlimcnp  25537  lgamgulmlem2  25601  lgseisenlem2  25946  dchrisumlema  26058  dchrisumlem2  26060  dchrisumlem3  26061  mptelee  26675  gropd  26810  grstructd  26811  isch3  29012  atom1d  30124  mo5f  30247  ssiun2sf  30305  ssrelf  30360  fmptcof2  30396  aciunf1lem  30401  nn0min  30531  fsumiunle  30540  esum2dlem  31346  fiunelros  31428  measiun  31472  bnj1385  32099  bnj1468  32113  bnj110  32125  bnj849  32192  bnj900  32196  bnj981  32217  bnj1014  32228  bnj1123  32253  bnj1128  32257  bnj1384  32299  bnj1489  32323  bnj1497  32327  setinds  33018  tfisg  33050  frpoinsg  33076  frinsg  33082  nosupbnd1  33209  nosupbnd2  33211  subtr  33657  subtr2  33658  currysetlem  34251  currysetlem1  34253  mptsnunlem  34613  finxpreclem2  34665  finxpreclem6  34671  ptrest  34885  poimirlem24  34910  poimirlem25  34911  poimirlem26  34912  poimirlem28  34914  fdc1  35015  ac6s6  35444  fsumshftd  36082  cdleme31sn1  37511  cdleme32fva  37567  cdlemk36  38043  fphpd  39406  monotuz  39531  monotoddzz  39533  oddcomabszz  39534  setindtrs  39615  aomclem6  39652  flcidc  39767  rababg  39926  ss2iundf  39997  binomcxplemnotnn0  40681  uzwo4  41308  fiiuncl  41320  disjf1  41436  disjinfi  41447  dmrelrnrel  41483  supxrgere  41594  supxrgelem  41598  supxrge  41599  supxrleubrnmptf  41720  monoordxr  41752  monoord2xr  41754  fsumclf  41843  fsummulc1f  41844  fsumnncl  41845  fsumsplit1  41846  fsumf1of  41848  fsumiunss  41849  fsumreclf  41850  fsumlessf  41851  fsumsermpt  41853  fmul01  41854  fmuldfeqlem1  41856  fmuldfeq  41857  fmul01lt1lem1  41858  fmul01lt1lem2  41859  fprodexp  41868  fprodabs2  41869  fprodcnlem  41873  climmulf  41878  climexp  41879  climsuse  41882  climrecf  41883  climinff  41885  climaddf  41889  mullimc  41890  idlimc  41900  neglimc  41921  addlimc  41922  0ellimcdiv  41923  limclner  41925  climsubmpt  41934  climreclf  41938  climeldmeqmpt  41942  climfveqmpt  41945  fnlimfvre  41948  climfveqf  41954  climfveqmpt3  41956  climeldmeqf  41957  limsupref  41959  limsupbnd1f  41960  climeqf  41962  climeldmeqmpt3  41963  climinf2  41981  climinf2mpt  41988  climinfmpt  41989  limsupmnf  41995  limsupequz  41997  limsupre2  41999  limsupequzmptf  42005  limsupre3  42007  cncfshift  42150  fprodcncf  42177  dvmptmulf  42215  dvnmptdivc  42216  dvnmul  42221  dvmptfprodlem  42222  dvmptfprod  42223  iblspltprt  42251  stoweidlem3  42282  stoweidlem26  42305  stoweidlem31  42310  stoweidlem34  42313  stoweidlem42  42321  stoweidlem43  42322  stoweidlem48  42327  stoweidlem51  42330  stoweidlem59  42338  fourierdlem86  42471  fourierdlem89  42474  fourierdlem91  42476  fourierdlem112  42497  sge0f1o  42658  sge0lempt  42686  sge0iunmptlemfi  42689  sge0iunmptlemre  42691  sge0fodjrnlem  42692  sge0iunmpt  42694  sge0ltfirpmpt2  42702  sge0isummpt2  42708  sge0xaddlem2  42710  sge0xadd  42711  meadjiun  42742  voliunsge0lem  42748  meaiunincf  42759  meaiuninc3  42761  meaiininc  42763  hoimbl2  42941  vonhoire  42948  vonn0ioo2  42966  vonn0icc2  42968  salpreimagelt  42980  salpreimalegt  42982  salpreimagtge  42996  salpreimaltle  42997  salpreimagtlt  43001  2reu8i  43306  eu2ndop1stv  43318  f1oresf1o2  43484  ichreuopeq  43629  reupr  43678  reuopreuprim  43682  2zrngmmgm  44211  nfsetrecs  44783  setrec2fun  44789