Theorem pldofph

Description: Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020)

	Ref	Expression
Hypotheses	pldofph.1	|- ( ta <-> ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) ) )
	pldofph.2	|- ph
	pldofph.3	|- ps
	pldofph.4	|- ch
	pldofph.5	|- th
Assertion	pldofph	|- ta

Proof

Step	Hyp	Ref	Expression
1		pldofph.1	|- ( ta <-> ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) ) )
2		pldofph.2	|- ph
3		pldofph.3	|- ps
4		pldofph.4	|- ch
5		pldofph.5	|- th
6	5	a1i	|- ( ch -> th )
7	2 4	2th	|- ( ph <-> ch )
8	3 5	2th	|- ( ps <-> th )
9	8	a1i	|- ( ( ph -> ps ) -> ( ps <-> th ) )
10	6 7 9	3pm3.2i	|- ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) )
11	1	bicomi	|- ( ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) ) <-> ta )
12	11	biimpi	|- ( ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) ) -> ta )
13	10 12	ax-mp	|- ta