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  4340  zeo3  16428  chnccat  18715  plngrotlem1  29145  tgaaddcpbl2  29233  angmgmaddov2lem  29267  angmgmaddcpbl  29270  angmgmaddcl  29271  hashxpe  33279  tlt2  33410  dflring3  33908  fsumcvg4  34461  chtvalz  35138  tsor1  38896  ts3or1  38902  aks4d1p5  42947