Metamath Proof Explorer


Theorem mdandyvr1

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

Ref Expression
Hypotheses mdandyvr1.1
|- ( ph <-> ze )
mdandyvr1.2
|- ( ps <-> si )
mdandyvr1.3
|- ( ch <-> ps )
mdandyvr1.4
|- ( th <-> ph )
mdandyvr1.5
|- ( ta <-> ph )
mdandyvr1.6
|- ( et <-> ph )
Assertion mdandyvr1
|- ( ( ( ( ch <-> si ) /\ ( th <-> ze ) ) /\ ( ta <-> ze ) ) /\ ( et <-> ze ) )

Proof

Step Hyp Ref Expression
1 mdandyvr1.1
 |-  ( ph <-> ze )
2 mdandyvr1.2
 |-  ( ps <-> si )
3 mdandyvr1.3
 |-  ( ch <-> ps )
4 mdandyvr1.4
 |-  ( th <-> ph )
5 mdandyvr1.5
 |-  ( ta <-> ph )
6 mdandyvr1.6
 |-  ( et <-> ph )
7 3 2 bitri
 |-  ( ch <-> si )
8 4 1 bitri
 |-  ( th <-> ze )
9 7 8 pm3.2i
 |-  ( ( ch <-> si ) /\ ( th <-> ze ) )
10 5 1 bitri
 |-  ( ta <-> ze )
11 9 10 pm3.2i
 |-  ( ( ( ch <-> si ) /\ ( th <-> ze ) ) /\ ( ta <-> ze ) )
12 6 1 bitri
 |-  ( et <-> ze )
13 11 12 pm3.2i
 |-  ( ( ( ( ch <-> si ) /\ ( th <-> ze ) ) /\ ( ta <-> ze ) ) /\ ( et <-> ze ) )