Theorem exmidd 909

Description: Law of excluded middle in a context. (Contributed by Mario Carneiro, 9-Feb-2017.)

Assertion

Ref	Expression
exmidd	⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓))

Proof of Theorem exmidd

Step	Hyp	Ref	Expression
1		exmid 908	. 2 ⊢ (𝜓 ∨ ¬ 𝜓)
2	1	a1i 11	1 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  rabxm  4343  zeo3  16551  chnccat  18850  plngrotlem1  29322  tgaaddcpbl2  29410  angmgmaddov2lem  29444  angmgmaddcpbl  29447  angmgmaddcl  29448  hashxpe  33495  tlt2  33626  dflring3  34133  fsumcvg4  34693  chtvalz  35369  tsor1  39345  ts3or1  39351  aks4d1p5  43396