Theorem an12 844

Description: Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position.

Assertion

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

Proof of Theorem an12

Step	Hyp	Ref	Expression
1		ancom 414	. . 3 |- ((ph /\ ps) <-> (ps /\ ph))
2	1	anbi1i 709	. 2 |- (((ph /\ ps) /\ ch) <-> ((ps /\ ph) /\ ch))
3		anass 633	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
4		anass 633	. 2 |- (((ps /\ ph) /\ ch) <-> (ps /\ (ph /\ ch)))
5	2, 3, 4	3bitr3i 293	1 |- ((ph /\ (ps /\ ch)) <-> (ps /\ (ph /\ ch)))

Syntax hints:   <-> wb 219   /\ wa 337

This theorem is referenced by:  an32 845  an13 847  an12s 851  an4 882  ceqsrexv 2634  2reuswap 2695  reuind 2696  sbccomglem 2757  elunirab 3379  axsep 3605  reuxfr2d 3990  reuxfr2 3991  elxp2 4152  elres 4368  dff1o2 4727  opabex3 4933  imaiun 4935  resoprab 5031  oprabval6g 5056  xpassen 5664  aceq5lem2 6190  distrpq 6585  genpass 6630  ltexprlem4 6663  suppsr2 6741  elreal 6768  rexuz2 7961  dffsum 8654  divalglem10 9299  isbasis2g 9732  tgval2 9738  tgval3 9746  basgen 9761  elresOLD 14454  tfrALTlem 14629  dffprod 15409  isfne2 16305  opabex3OLD 16525  prter3 17110  islpln5 17966  islvol5 18011  cdleme0nex 18661

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 220  df-an 339

Copyright terms: Public domain