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

Proof

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