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

Metamath Proof Explorer

Theorem nf3and

Description: Deduction form of bound-variable hypothesis builder nf3an . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 16-Oct-2016)

Ref Expression
Hypotheses nfand.1 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
nfand.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
nfand.3 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜃 )
Assertion nf3and ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )

Proof

Step Hyp Ref Expression
1 nfand.1 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
2 nfand.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
3 nfand.3 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜃 )
4 df-3an ⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
5 1 2 nfand ⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ) )
6 5 3 nfand ⊢ ( 𝜑 → Ⅎ 𝑥 ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
7 4 6 nfxfrd ⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )