Metamath Proof Explorer


Theorem hb3an

Description: If x is not free in ph , ps , and ch , it is not free in ( ph /\ ps /\ ch ) . (Contributed by NM, 14-Sep-2003) (Proof shortened by Wolf Lammen, 2-Jan-2018)

Ref Expression
Hypotheses hb.1 φxφ
hb.2 ψxψ
hb.3 χxχ
Assertion hb3an φψχxφψχ

Proof

Step Hyp Ref Expression
1 hb.1 φxφ
2 hb.2 ψxψ
3 hb.3 χxχ
4 1 nf5i xφ
5 2 nf5i xψ
6 3 nf5i xχ
7 4 5 6 nf3an xφψχ
8 7 nf5ri φψχxφψχ