Theorem _nf_clos_or ≪ | index | src | ≫

\nf闭包\or（不可引用）

theorem _nf_clos_or {x: set} (A B: wff x):
  $ \nf x A $ >
  $ \nf x B $ >
  $ \nf x (A \or B) $;

Step	Hyp	Ref	Expression
1		hyp h1	\nf x A
2	1	_nf_clos_neg	\nf x \neg A
3		hyp h2	\nf x B
4	2, 3	_nf_clos_imp	\nf x (\neg A \imp B)
5	4	conv or	\nf x (A \or B)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4)