Metamath Proof Explorer


Theorem mdandyv6

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 mdandyv6.1
|- ( ph <-> F. )
mdandyv6.2
|- ( ps <-> T. )
mdandyv6.3
|- ( ch <-> F. )
mdandyv6.4
|- ( th <-> T. )
mdandyv6.5
|- ( ta <-> T. )
mdandyv6.6
|- ( et <-> F. )
Assertion mdandyv6
|- ( ( ( ( ch <-> ph ) /\ ( th <-> ps ) ) /\ ( ta <-> ps ) ) /\ ( et <-> ph ) )

Proof

Step Hyp Ref Expression
1 mdandyv6.1
 |-  ( ph <-> F. )
2 mdandyv6.2
 |-  ( ps <-> T. )
3 mdandyv6.3
 |-  ( ch <-> F. )
4 mdandyv6.4
 |-  ( th <-> T. )
5 mdandyv6.5
 |-  ( ta <-> T. )
6 mdandyv6.6
 |-  ( et <-> F. )
7 3 1 bothfbothsame
 |-  ( ch <-> ph )
8 4 2 bothtbothsame
 |-  ( th <-> ps )
9 7 8 pm3.2i
 |-  ( ( ch <-> ph ) /\ ( th <-> ps ) )
10 5 2 bothtbothsame
 |-  ( ta <-> ps )
11 9 10 pm3.2i
 |-  ( ( ( ch <-> ph ) /\ ( th <-> ps ) ) /\ ( ta <-> ps ) )
12 6 1 bothfbothsame
 |-  ( et <-> ph )
13 11 12 pm3.2i
 |-  ( ( ( ( ch <-> ph ) /\ ( th <-> ps ) ) /\ ( ta <-> ps ) ) /\ ( et <-> ph ) )