Theorem an4 564

Description: Rearrangement of 4 conjuncts.

Assertion

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

Proof of Theorem an4

Step	Hyp	Ref	Expression
1		an12 542	. . 3 |- ((ps /\ (ch /\ th)) <-> (ch /\ (ps /\ th)))
2	1	anbi2i 538	. 2 |- ((ph /\ (ps /\ (ch /\ th))) <-> (ph /\ (ch /\ (ps /\ th))))
3		anass 487	. 2 |- (((ph /\ ps) /\ (ch /\ th)) <-> (ph /\ (ps /\ (ch /\ th))))
4		anass 487	. 2 |- (((ph /\ ch) /\ (ps /\ th)) <-> (ph /\ (ch /\ (ps /\ th))))
5	2, 3, 4	3bitr4i 200	1 |- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (ps /\ th)))

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

This theorem is referenced by:  an42 565  an4s 566  anandi 568  anandir 569  rnlem 853  rnlemOLD 854  an6 1177  euanOLD 1828  2eu1 1853  2eu4 1856  reean 2247  reeanOLD 2248  reu2 2442  rmo4 2445  opelxpOLD 4037  inxp 4109  inxpOLD 4110  xp11 4347  fununi 4481  2elresin 4524  fun 4580  finOLD 4594  tfrlem7 5125  th3qlem1 5373  xpmapenlem5 5594  abfii2 5652  aceq5lem1 5897  zorn2lem6 5955  nnaun 6089  genpass 6264  distrlem5pr 6283  mulgt0sr 6366  iooin 7539  creur 7992  creui 7993  replim 8011  xpcn 9254  ocsh 10789  5oalem6 11239  cvnbtwn4 11861  superpos 11926  cdj3i 12013  xporderlem 13948  poxp 13949  poseq 13954  axfelem14 14044  qusp 14908  unirep 15664  resoprab2 15710  inixp 15722  blhalf 15846  haustlmu 15906  txmet 15925  abl4pnp 16037  keridl 16180  ispridlc 16218  an43OLD 16236  prtlem70 16238  cvrnbtwn4 16996  linepsub 17232  pmapsub 17250  pmapjoin 17313

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