Metamath Proof Explorer

Theorem mdandyv1

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 mdandyv1.1 ⊢ φ ↔ ⊥
mdandyv1.2 ⊢ ψ ↔ ⊤
mdandyv1.3 ⊢ χ ↔ ⊤
mdandyv1.4 ⊢ θ ↔ ⊥
mdandyv1.5 ⊢ τ ↔ ⊥
mdandyv1.6 ⊢ η ↔ ⊥
Assertion mdandyv1 ⊢ χ ↔ ψ ∧ θ ↔ φ ∧ τ ↔ φ ∧ η ↔ φ

Proof

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