Theorem rnlem 853

Description: Lemma used in construction of real numbers. (The proof was shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
rnlem	|- (((ph /\ ps) /\ (ch /\ th)) <-> (((ph /\ ch) /\ (ps /\ th)) /\ ((ph /\ th) /\ (ps /\ ch))))

Proof of Theorem rnlem

Step	Hyp	Ref	Expression
1		an4 564	. . . 4 |- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (ps /\ th)))
2	1	biimpi 168	. . 3 |- (((ph /\ ps) /\ (ch /\ th)) -> ((ph /\ ch) /\ (ps /\ th)))
3		an42 565	. . . 4 |- (((ph /\ th) /\ (ps /\ ch)) <-> ((ph /\ ps) /\ (ch /\ th)))
4	3	biimpri 169	. . 3 |- (((ph /\ ps) /\ (ch /\ th)) -> ((ph /\ th) /\ (ps /\ ch)))
5	2, 4	jca 310	. 2 |- (((ph /\ ps) /\ (ch /\ th)) -> (((ph /\ ch) /\ (ps /\ th)) /\ ((ph /\ th) /\ (ps /\ ch))))
6	3	biimpi 168	. . 3 |- (((ph /\ th) /\ (ps /\ ch)) -> ((ph /\ ps) /\ (ch /\ th)))
7	6	adantl 424	. 2 |- ((((ph /\ ch) /\ (ps /\ th)) /\ ((ph /\ th) /\ (ps /\ ch))) -> ((ph /\ ps) /\ (ch /\ th)))
8	5, 7	impbii 174	1 |- (((ph /\ ps) /\ (ch /\ th)) <-> (((ph /\ ch) /\ (ps /\ th)) /\ ((ph /\ th) /\ (ps /\ ch))))

Syntax hints:   <-> wb 163   /\ wa 240

This theorem is referenced by:  mulcmpblnr 6335

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain