Theorem nford 1456

Description: If in a context x is not free in ps and ch, it is not free in (ps \/ ch). (Contributed by Jim Kingdon, 29-Oct-2019.)

Hypotheses

Ref	Expression
nford.1	|- (ph -> F/xps)
nford.2	|- (ph -> F/xch)

Assertion

Ref	Expression
nford	|- (ph -> F/x(ps \/ ch))

Proof of Theorem nford

Step	Hyp	Ref	Expression
1		nford.1	. . . . 5 |- (ph -> F/xps)
2		nford.2	. . . . 5 |- (ph -> F/xch)
3		df-nf 1347	. . . . . . 7 |- ( F/xps <-> A.x(ps -> A.xps))
4		df-nf 1347	. . . . . . 7 |- ( F/xch <-> A.x(ch -> A.xch))
5	3, 4	anbi12i 433	. . . . . 6 |- (( F/xps /\ F/xch) <-> (A.x(ps -> A.xps) /\ A.x(ch -> A.xch)))
6	5	biimpi 113	. . . . 5 |- (( F/xps /\ F/xch) -> (A.x(ps -> A.xps) /\ A.x(ch -> A.xch)))
7	1, 2, 6	syl2anc 391	. . . 4 |- (ph -> (A.x(ps -> A.xps) /\ A.x(ch -> A.xch)))
8		19.26 1367	. . . 4 |- (A.x((ps -> A.xps) /\ (ch -> A.xch)) <-> (A.x(ps -> A.xps) /\ A.x(ch -> A.xch)))
9	7, 8	sylibr 137	. . 3 |- (ph -> A.x((ps -> A.xps) /\ (ch -> A.xch)))
10		orc 632	. . . . . . 7 |- (ps -> (ps \/ ch))
11	10	alimi 1341	. . . . . 6 |- (A.xps -> A.x(ps \/ ch))
12	11	imim2i 12	. . . . 5 |- ((ps -> A.xps) -> (ps -> A.x(ps \/ ch)))
13		olc 631	. . . . . . 7 |- (ch -> (ps \/ ch))
14	13	alimi 1341	. . . . . 6 |- (A.xch -> A.x(ps \/ ch))
15	14	imim2i 12	. . . . 5 |- ((ch -> A.xch) -> (ch -> A.x(ps \/ ch)))
16	12, 15	jaao 638	. . . 4 |- (((ps -> A.xps) /\ (ch -> A.xch)) -> ((ps \/ ch) -> A.x(ps \/ ch)))
17	16	alimi 1341	. . 3 |- (A.x((ps -> A.xps) /\ (ch -> A.xch)) -> A.x((ps \/ ch) -> A.x(ps \/ ch)))
18	9, 17	syl 14	. 2 |- (ph -> A.x((ps \/ ch) -> A.x(ps \/ ch)))
19		df-nf 1347	. 2 |- ( F/x(ps \/ ch) <-> A.x((ps \/ ch) -> A.x(ps \/ ch)))
20	18, 19	sylibr 137	1 |- (ph -> F/x(ps \/ ch))

Syntax hints:   -> wi 4   /\ wa 97   \/ wo 628  A.wal 1240   F/wnf 1346

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-gen 1335

This theorem depends on definitions:  df-bi 110  df-nf 1347

This theorem is referenced by:  nfifd  3349