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 ⊢ χ ↔ ψ ∧ θ ↔ ψ ∧ τ ↔ ψ ∧ η ↔ ψ