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	⊢ ( 𝜏 ↔ ( ( 𝜒 → 𝜃 ) ∧ ( 𝜑 ↔ 𝜒 ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜓 ↔ 𝜃 ) ) ) )
	pldofph.2	⊢ 𝜑
	pldofph.3	⊢ 𝜓
	pldofph.4	⊢ 𝜒
	pldofph.5	⊢ 𝜃
Assertion	pldofph	⊢ 𝜏

Proof

Step	Hyp	Ref	Expression
1		pldofph.1	⊢ ( 𝜏 ↔ ( ( 𝜒 → 𝜃 ) ∧ ( 𝜑 ↔ 𝜒 ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜓 ↔ 𝜃 ) ) ) )
2		pldofph.2	⊢ 𝜑
3		pldofph.3	⊢ 𝜓
4		pldofph.4	⊢ 𝜒
5		pldofph.5	⊢ 𝜃
6	5	a1i	⊢ ( 𝜒 → 𝜃 )
7	2 4	2th	⊢ ( 𝜑 ↔ 𝜒 )
8	3 5	2th	⊢ ( 𝜓 ↔ 𝜃 )
9	8	a1i	⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜓 ↔ 𝜃 ) )
10	6 7 9	3pm3.2i	⊢ ( ( 𝜒 → 𝜃 ) ∧ ( 𝜑 ↔ 𝜒 ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜓 ↔ 𝜃 ) ) )
11	1	bicomi	⊢ ( ( ( 𝜒 → 𝜃 ) ∧ ( 𝜑 ↔ 𝜒 ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜓 ↔ 𝜃 ) ) ) ↔ 𝜏 )
12	11	biimpi	⊢ ( ( ( 𝜒 → 𝜃 ) ∧ ( 𝜑 ↔ 𝜒 ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜓 ↔ 𝜃 ) ) ) → 𝜏 )
13	10 12	ax-mp	⊢ 𝜏