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  4339  zeo3  16516  chnccat  18809  plngrotlem1  29274  tgaaddcpbl2  29362  angmgmaddov2lem  29396  angmgmaddcpbl  29399  angmgmaddcl  29400  hashxpe  33449  tlt2  33580  dflring3  34079  fsumcvg4  34632  chtvalz  35308  tsor1  39216  ts3or1  39222  aks4d1p5  43267