Theorem pldofph 44440

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

Hypotheses

Ref	Expression
pldofph.1	⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃))))
pldofph.2	⊢ 𝜑
pldofph.3	⊢ 𝜓
pldofph.4	⊢ 𝜒
pldofph.5	⊢ 𝜃

Assertion

Ref	Expression
pldofph	⊢ 𝜏

Proof of Theorem pldofph

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  plvcofph  44441  plvcofphax  44442