Theorem 19.21a3con13v 5828

Description: Closed form of 19.21ai 1345 with 2 additional conjuncts having no occurences of the quantifying variable. This proof is 19.21a3con13vVD 16676 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.)

Assertion

Ref	Expression
19.21a3con13v	|- ((ph -> A.xph) -> ((ps /\ ph /\ ch) -> A.x(ps /\ ph /\ ch)))

Distinct variable groups:   ps,x   ch,x

Proof of Theorem 19.21a3con13v

Step	Hyp	Ref	Expression
1		simp1 876	. . . . 5 |- ((ps /\ ph /\ ch) -> ps)
2	1	a1i 8	. . . 4 |- ((ph -> A.xph) -> ((ps /\ ph /\ ch) -> ps))
3		ax-17 1317	. . . 4 |- (ps -> A.xps)
4	2, 3	syl6 25	. . 3 |- ((ph -> A.xph) -> ((ps /\ ph /\ ch) -> A.xps))
5		simp2 877	. . . 4 |- ((ps /\ ph /\ ch) -> ph)
6	5	imim1i 19	. . 3 |- ((ph -> A.xph) -> ((ps /\ ph /\ ch) -> A.xph))
7		simp3 878	. . . . 5 |- ((ps /\ ph /\ ch) -> ch)
8	7	a1i 8	. . . 4 |- ((ph -> A.xph) -> ((ps /\ ph /\ ch) -> ch))
9		ax-17 1317	. . . 4 |- (ch -> A.xch)
10	8, 9	syl6 25	. . 3 |- ((ph -> A.xph) -> ((ps /\ ph /\ ch) -> A.xch))
11	4, 6, 10	3jcad 1051	. 2 |- ((ph -> A.xph) -> ((ps /\ ph /\ ch) -> (A.xps /\ A.xph /\ A.xch)))
12		19.26-3an 1418	. 2 |- (A.x(ps /\ ph /\ ch) <-> (A.xps /\ A.xph /\ A.xch))
13	11, 12	syl6ibr 230	1 |- ((ph -> A.xph) -> ((ps /\ ph /\ ch) -> A.x(ps /\ ph /\ ch)))

Syntax hints:   -> wi 3   /\ w3a 858  A.wal 1296

This theorem is referenced by:  tratrb 5831  tratrbVD 16685

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain