Theorem an12 495

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 446	. . 3 |- ((ph /\ ps) <-> (ps /\ ph))
2	1	anbi1i 492	. 2 |- (((ph /\ ps) /\ ch) <-> ((ps /\ ph) /\ ch))
3		anass 450	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
4		anass 450	. 2 |- (((ps /\ ph) /\ ch) <-> (ps /\ (ph /\ ch)))
5	2, 3, 4	3bitr3i 188	1 |- ((ph /\ (ps /\ ch)) <-> (ps /\ (ph /\ ch)))

Syntax hints:   <-> wb 153   /\ wa 230

This theorem is referenced by:  an1s 497  an4 517  r19.29 1803  ceqsrexv 1936  2reuswap 1984  sbccomglem 2038  elunirab 2568  dfiun2g 2640  axsep 2757  reuxfr2 2960  elxp2 3260  fcoi2 3703  f1o2 3750  f1o5 3754  imaiun 3921  resoprab 4067  oprabval6g 4090  2ndconst 4155  xpassen 4504  aceq5lem2 4798  distrpq 5132  genpass 5177  ltexprlem4 5210  suppsr2 5288  elreal 5315  rexuz2 6471  dffsum 7088  isbasis2g 7701  tgval2 7706  tgval3 7714  basgen 7729

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 154  df-an 232

Copyright terms: Public domain