Theorem ex_or_distrs_nfls ≪ | index | src | ≫

\ex\or分配右侧(左侧不出现)

theorem ex_or_distrs_nfls {x: set} (A B: wff x):
  $ \nf x A $ >
  $ \ex x (A \or B) \iff A \or \ex x B $;
StepHypRefExpression
1 hyp n 
\nf x A
2 1 _nf_clos_neg 
\nf x \neg A
3 2 ex_imp_distrs_nfls 
\ex x (\neg A \imp B) \iff \neg A \imp \ex x B
4 3 conv or 
\ex x (A \or B) \iff A \or \ex x B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12)