Theorem _nf_clos_and ≪ | index | src | ≫

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

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

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

Axiom use

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