Theorem fo_or_distrs_nfls ≪ | index | src | ≫

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

theorem fo_or_distrs_nfls {x: set} (A B: wff x):
  $ \nf x A $ >
  $ \fo x (A \or B) \iff A \or \fo x B $;
StepHypRefExpression
1 hyp n 
\nf x A
2 1 _nf_clos_neg 
\nf x \neg A
3 2 fo_imp_distrs_nfls 
\fo x (\neg A \imp B) \iff \neg A \imp \fo x B
4 3 conv or 
\fo x (A \or B) \iff A \or \fo 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)