Metamath Proof Explorer

Theorem mdandyv15

Description: Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016)

Ref Expression
Hypotheses mdandyv15.1 ⊢φ↔⊥
mdandyv15.2 ⊢ψ↔⊤
mdandyv15.3 ⊢χ↔⊤
mdandyv15.4 ⊢θ↔⊤
mdandyv15.5 ⊢τ↔⊤
mdandyv15.6 ⊢η↔⊤
Assertion mdandyv15 ⊢χ↔ψ∧θ↔ψ∧τ↔ψ∧η↔ψ

Proof

Step Hyp Ref Expression
1 mdandyv15.1 ⊢φ↔⊥
2 mdandyv15.2 ⊢ψ↔⊤
3 mdandyv15.3 ⊢χ↔⊤
4 mdandyv15.4 ⊢θ↔⊤
5 mdandyv15.5 ⊢τ↔⊤
6 mdandyv15.6 ⊢η↔⊤
7 3 2 bothtbothsame ⊢χ↔ψ
8 4 2 bothtbothsame ⊢θ↔ψ
9 7 8 pm3.2i ⊢χ↔ψ∧θ↔ψ
10 5 2 bothtbothsame ⊢τ↔ψ
11 9 10 pm3.2i ⊢χ↔ψ∧θ↔ψ∧τ↔ψ
12 6 2 bothtbothsame ⊢η↔ψ
13 11 12 pm3.2i ⊢χ↔ψ∧θ↔ψ∧τ↔ψ∧η↔ψ