Theorem an12 487

Description: A rearrangement of conjuncts.

Assertion

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

Proof of Theorem an12

Step	Hyp	Ref	Expression
1		ancom 437	. . 3 |- ((ph /\ ps) <-> (ps /\ ph))
2	1	anbi1i 484	. 2 |- (((ph /\ ps) /\ ch) <-> ((ps /\ ph) /\ ch))
3		anass 441	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
4		anass 441	. 2 |- (((ps /\ ph) /\ ch) <-> (ps /\ (ph /\ ch)))
5	2, 3, 4	3bitr3i 179	1 |- ((ph /\ (ps /\ ch)) <-> (ps /\ (ph /\ ch)))

Syntax hints:   <-> wb 144   /\ wa 221

This theorem is referenced by:  an1s 489  an4 509  r19.29 1802  ceqsrexv 1935  2reuswap 1983  sbccomglem 2038  elunirab 2580  dfiun2g 2654  axsep 2776  reuxfr2 3126  elxp2 3284  iunfopab 3719  fcoi2 3753  dff1o2 3801  dff1o5 3805  imaiun 3978  resoprab 4069  oprabval6g 4093  xpassen 4582  aceq5lem2 4882  distrpq 5221  genpass 5266  ltexprlem4 5299  suppsr2 5377  elreal 5404  rexuz2 6572  dffsum 7201  isbasis2g 7824  tgval2 7829  tgval3 7837  basgen 7852  isfne2 11542  opabex3 11806

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 145  df-an 223

Copyright terms: Public domain