Metamath Proof Explorer


Theorem mdandyv2

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 mdandyv2.1 φ
mdandyv2.2 ψ
mdandyv2.3 χ
mdandyv2.4 θ
mdandyv2.5 τ
mdandyv2.6 η
Assertion mdandyv2 χφθψτφηφ

Proof

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