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

Proof

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