Theorem an12 567

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 266	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2	1	anbi1i 462	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ps /\ ph ) /\ ch ) )
3		anass 405	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
4		anass 405	. 2 |- ( ( ( ps /\ ph ) /\ ch ) <-> ( ps /\ ( ph /\ ch ) ) )
5	2, 3, 4	3bitr3i 210	1 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ps /\ ( ph /\ ch ) ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  an32  568  an13  569  an12s  571  an4  592  ceqsrexv  2956  rmoan  3026  2reuswapdc  3030  reuind  3031  2rmorex  3032  sbccomlem  3126  elunirab  3948  rexxfrd  4611  opeliunxp  4832  elres  5101  resoprab  6187  ov6g  6230  opabex3d  6354  opabex3  6355  xpassen  7132  distrnqg  7760  distrnq0  7832  rexuz2  9997  2clim  12092  bitsmod  12748  issubrg  14638  isbasis2g  15271  tgval2  15277