Theorem an12 486

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 483	. 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	3bitr3 181	1 |- ((ph /\ (ps /\ ch)) <-> (ps /\ (ph /\ ch)))

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

This theorem is referenced by:  an1s 488  an4 508  r19.29 1759  ceqsrexv 1892  2reuswap 1940  sbccomglem 1991  elunirab 2518  dfiun2g 2590  axsep 2707  reuxfr2 2909  elxp2 3209  fcoi2 3652  f1o2 3699  f1o5 3703  imaiun 3870  resoprab 4015  oprabval6g 4038  2ndconst 4103  xpassen 4447  aceq5lem2 4746  distrpq 5079  genpass 5124  ltexprlem4 5157  suppsr2 5235  elreal 5262  rexuz2 6446  dffsum 6998  isbasis2g 7611  tgval2t 7616  tgval3t 7624  basgent 7639

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