Metamath Proof Explorer

Theorem mdandyv0

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

Proof

Step Hyp Ref Expression
1 mdandyv0.1 ⊢φ↔⊥
2 mdandyv0.2 ⊢ψ↔⊤
3 mdandyv0.3 ⊢χ↔⊥
4 mdandyv0.4 ⊢θ↔⊥
5 mdandyv0.5 ⊢τ↔⊥
6 mdandyv0.6 ⊢η↔⊥
7 3 1 bothfbothsame ⊢χ↔φ
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 ⊢χ↔φ∧θ↔φ∧τ↔φ∧η↔φ