Theorem ndnfrv-P7.1 826

Description: Natural Deduction: Effective Non-Freeness Rule 1.

If '𝑥' does not occur in '𝜑', then '𝑥' is effectively not free in '𝜑'.

Assertion

Ref	Expression
ndnfrv-P7.1	⊢ Ⅎ𝑥𝜑

Distinct variable group:   𝜑,𝑥

Proof of Theorem ndnfrv-P7.1

Step	Hyp	Ref	Expression
1		nfrv-P6 686	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:  Ⅎwff-nfree 681

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682

This theorem is referenced by:  ndnfrall2-P7.9.VR12of2  860  ndnfrex2-P7.10.VR12of2  861  ndnfrleq-P7.11.VR  862  ndpsub1-P7.13.VR  863  ndalli-P7.17.VR1of2  864  ndalli-P7.17.VR2of2  865  ndalli-P7.17.VR12of2  866  ndexew-P7.VR1of3  868  ndexew-P7.VR2of3  869  ndexew-P7.VR3of3  870  ndexew-P7.VR12of3  871  ndexew-P7.VR13of3  872  ndexew-P7.VR23of3  873  ndexew-P7.VR123of3  874  ndalli-P7.17.RC.VR  884  ndexew-P7.RC.VR1of2  888  ndexew-P7.RC.VR2of2  889  ndexew-P7.RC.VR12of2  890  nfrthm-P7  926  axL5-P7  934  axL5ex-P7  935  psubid-P7  940  lemma-L7.02a  944  alloverimex-P7.GENF.RC  950  exia-P7.RC  954  allnegex-P7-L1  956  lemma-L7.03  962  alloverim-P7.GENF.RC  972  suball-P7.RC  974  alli-P7r.VR  991  exe-P7r.VR1of2  999  exe-P7r.VR2of2  1000  exe-P7r.VR12of2  1001  exe-P7r.RC  1002  exe-P7r.RC.VR  1003  allic-P7.VR1of2  1008  allic-P7.VR2of2  1009  allic-P7.VR12of2  1010  exia-P7r.VR1of2  1012  exia-P7r.VR2of2  1013  exia-P7r.VR12of2  1014  exia-P7r.RC.VR  1016  dalloverim-P7.GENF.RC  1027  dalloverimex-P7.GENF.RC  1038  suball-P7r.VR  1040  subex-P7.VR  1043  subex-P7.RC  1044  exnegallint-P7  1047  qimeqalla-P7.VR  1051  qimeqallb-P7r.VR  1053  cbvall-P7.VR1of2  1062  cbvall-P7.VR2of2  1063  cbvall-P7.VR12of2  1064  cbvex-P7.VR1of2  1067  cbvex-P7.VR2of2  1068  cbvex-P7.VR12of2  1069  cbvallpsub-P7.VR  1071  cbvexpsub-P7.VR  1073  example-E7.1a  1074  nfrgen-P7.VR  1077  nfrexgen-P8.VR  1081  nfrexgen-P8.RC.VR  1083  nfrexall-P8.VR  1087  nfrexall-P8.RC.VR  1089  nfrexall-P8.CL.VR  1091  qremall-P8.VR  1102  qremex-P8.VR  1104  qswap-P8.VR  1106  nfrcond-P8.VR  1109  nfrzero-P8  1117  nfrvar-P8  1118  nfrsucc-P8  1119  nfradd-P8  1120  nfrmult-P8  1121