Theorem motr 34127

Description: Lemma for ~? trcoss . (Contributed by Peter Mazsa, 2-Oct-2018.)

Assertion

Ref	Expression
motr	|- ( E* x ps -> ( ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) -> E. x ( ph /\ ch ) ) )

Proof of Theorem motr

Step	Hyp	Ref	Expression
1		exancom 1787	. . . . . . 7 |- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
2	1	anbi1i 731	. . . . . 6 |- ( ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) <-> ( E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) )
3	2	anbi2i 730	. . . . 5 |- ( ( E* x ps /\ ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) ) <-> ( E* x ps /\ ( E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) ) )
4		3anass 1042	. . . . 5 |- ( ( E* x ps /\ E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) <-> ( E* x ps /\ ( E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) ) )
5	3, 4	bitr4i 267	. . . 4 |- ( ( E* x ps /\ ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) ) <-> ( E* x ps /\ E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) )
6		mopick2 2540	. . . 4 |- ( ( E* x ps /\ E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) -> E. x ( ps /\ ph /\ ch ) )
7	5, 6	sylbi 207	. . 3 |- ( ( E* x ps /\ ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) ) -> E. x ( ps /\ ph /\ ch ) )
8		3anass 1042	. . . . 5 |- ( ( ps /\ ph /\ ch ) <-> ( ps /\ ( ph /\ ch ) ) )
9	8	exbii 1774	. . . 4 |- ( E. x ( ps /\ ph /\ ch ) <-> E. x ( ps /\ ( ph /\ ch ) ) )
10		exsimpr 1796	. . . 4 |- ( E. x ( ps /\ ( ph /\ ch ) ) -> E. x ( ph /\ ch ) )
11	9, 10	sylbi 207	. . 3 |- ( E. x ( ps /\ ph /\ ch ) -> E. x ( ph /\ ch ) )
12	7, 11	syl 17	. 2 |- ( ( E* x ps /\ ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) ) -> E. x ( ph /\ ch ) )
13		impexp 462	. 2 |- ( ( ( E* x ps /\ ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) ) -> E. x ( ph /\ ch ) ) <-> ( E* x ps -> ( ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) -> E. x ( ph /\ ch ) ) ) )
14	12, 13	mpbi 220	1 |- ( E* x ps -> ( ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) -> E. x ( ph /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   E.wex 1704   E*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-eu 2474  df-mo 2475

This theorem is referenced by: (None)