This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nf3or

Description: If x is not free in ph , ps , and ch , then it is not free in ( ph \/ ps \/ ch ) . (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypotheses nf.1 ⊢ Ⅎ 𝑥 𝜑
nf.2 ⊢ Ⅎ 𝑥 𝜓
nf.3 ⊢ Ⅎ 𝑥 𝜒
Assertion nf3or Ⅎ 𝑥 ( 𝜑 ∨ 𝜓 ∨ 𝜒 )

Proof

Step Hyp Ref Expression
1 nf.1 ⊢ Ⅎ 𝑥 𝜑
2 nf.2 ⊢ Ⅎ 𝑥 𝜓
3 nf.3 ⊢ Ⅎ 𝑥 𝜒
4 df-3or ⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) )
5 1 2 nfor ⊢ Ⅎ 𝑥 ( 𝜑 ∨ 𝜓 )
6 5 3 nfor ⊢ Ⅎ 𝑥 ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 )
7 4 6 nfxfr ⊢ Ⅎ 𝑥 ( 𝜑 ∨ 𝜓 ∨ 𝜒 )