Theorem an12 484

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 435	. . 3 |- ((ph /\ ps) <-> (ps /\ ph))
2	1	anbi1i 481	. 2 |- (((ph /\ ps) /\ ch) <-> ((ps /\ ph) /\ ch))
3		anass 439	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
4		anass 439	. 2 |- (((ps /\ ph) /\ ch) <-> (ps /\ (ph /\ ch)))
5	2, 3, 4	3bitr3 181	1 |- ((ph /\ (ps /\ ch)) <-> (ps /\ (ph /\ ch)))

Syntax hints:   <-> wb 146   /\ wa 223

This theorem is referenced by:  an1s 486  an4 506  r19.29 1753  ceqsrexv 1885  2reuswap 1933  sbccomglem 1984  elunirab 2509  dfiun2g 2581  axsep 2697  reuxfr2 2898  elxp2 3198  fcoi2 3637  f1o2 3684  f1o5 3688  imaiun 3855  resoprab 4000  oprabval6g 4023  2ndconst 4087  xpassen 4427  aceq5lem2 4716  distrpq 5047  genpass 5092  ltexprlem4 5125  suppsr2 5203  elreal 5230  rexuz2 6385  dffsum 6944  isbasis2g 7562  tgval2t 7567  tgval3t 7575  basgent 7590

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 147  df-an 225

Copyright terms: Public domain