Theorem an12 838

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. (Contributed by NM, 12-Mar-1995.)

Assertion

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

Proof of Theorem an12

Step	Hyp	Ref	Expression
1		ancom 466	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2	1	anbi1i 731	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ps /\ ph ) /\ ch ) )
3		anass 681	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
4		anass 681	. 2 |- ( ( ( ps /\ ph ) /\ ch ) <-> ( ps /\ ( ph /\ ch ) ) )
5	2, 3, 4	3bitr3i 290	1 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ps /\ ( ph /\ ch ) ) )

Syntax hints:   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  an32  839  an13  840  an12s  843  an4  865  ceqsrexv  3336  rmoan  3406  2reuswap  3410  reuind  3411  sbccomlem  3508  elunirab  4448  axsep  4780  reuxfr2d  4891  opeliunxp  5170  elres  5435  resoprab  6756  elrnmpt2res  6774  ov6g  6798  opabex3d  7145  opabex3  7146  dfrecs3  7469  oeeu  7683  xpassen  8054  omxpenlem  8061  dfac5lem2  8947  ltexprlem4  9861  rexuz2  11739  2clim  14303  divalglem10  15125  bitsmod  15158  isssc  16480  eldmcoa  16715  issubrg  18780  isbasis2g  20752  tgval2  20760  is1stc2  21245  elflim2  21768  i1fres  23472  dvdsflsumcom  24914  vmasum  24941  logfac2  24942  axcontlem2  25845  fusgr2wsp2nb  27198  2reuswap2  29328  reuxfr3d  29329  1stpreima  29484  bnj849  30995  elima4  31679  elfuns  32022  brimg  32044  dfrecs2  32057  dfrdg4  32058  bj-axsep  32793  bj-restuni  33050  mptsnunlem  33185  relowlpssretop  33212  poimirlem27  33436  sstotbnd3  33575  an12i  33900  selconj  33902  eldmqsres  34051  islshpat  34304  islpln5  34821  islvol5  34865  cdleme0nex  35577  dicelval3  36469  mapdordlem1a  36923  2rmoswap  41184  elpglem3  42456