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	$$⊢\tau \leftrightarrow \left(\left(\chi \to \theta \right)\wedge \left(\phi \leftrightarrow \chi \right)\wedge \left(\left(\phi \to \psi \right)\to \left(\psi \leftrightarrow \theta \right)\right)\right)$$
	pldofph.2	$$⊢\phi$$
	pldofph.3	$$⊢\psi$$
	pldofph.4	$$⊢\chi$$
	pldofph.5	$$⊢\theta$$
Assertion	pldofph	$$⊢\tau$$

Proof

Step	Hyp	Ref	Expression
1		pldofph.1	$$⊢\tau \leftrightarrow \left(\left(\chi \to \theta \right)\wedge \left(\phi \leftrightarrow \chi \right)\wedge \left(\left(\phi \to \psi \right)\to \left(\psi \leftrightarrow \theta \right)\right)\right)$$
2		pldofph.2	$$⊢\phi$$
3		pldofph.3	$$⊢\psi$$
4		pldofph.4	$$⊢\chi$$
5		pldofph.5	$$⊢\theta$$
6	5	a1i	$$⊢\chi \to \theta$$
7	2 4	2th	$$⊢\phi \leftrightarrow \chi$$
8	3 5	2th	$$⊢\psi \leftrightarrow \theta$$
9	8	a1i	$$⊢\left(\phi \to \psi \right)\to \left(\psi \leftrightarrow \theta \right)$$
10	6 7 9	3pm3.2i	$$⊢\left(\left(\chi \to \theta \right)\wedge \left(\phi \leftrightarrow \chi \right)\wedge \left(\left(\phi \to \psi \right)\to \left(\psi \leftrightarrow \theta \right)\right)\right)$$
11	1	bicomi	$$⊢\left(\left(\chi \to \theta \right)\wedge \left(\phi \leftrightarrow \chi \right)\wedge \left(\left(\phi \to \psi \right)\to \left(\psi \leftrightarrow \theta \right)\right)\right)\leftrightarrow \tau$$
12	11	biimpi	$$⊢\left(\left(\chi \to \theta \right)\wedge \left(\phi \leftrightarrow \chi \right)\wedge \left(\left(\phi \to \psi \right)\to \left(\psi \leftrightarrow \theta \right)\right)\right)\to \tau$$
13	10 12	ax-mp	$$⊢\tau$$