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  16507  chnccat  18800  plngrotlem1  29265  tgaaddcpbl2  29353  angmgmaddov2lem  29387  angmgmaddcpbl  29390  angmgmaddcl  29391  hashxpe  33399  tlt2  33530  dflring3  34029  fsumcvg4  34582  chtvalz  35258  tsor1  39079  ts3or1  39085  aks4d1p5  43130