Theorem an12 561

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

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an32  562  an13  563  an12s  565  an4  586  ceqsrexv  2894  rmoan  2964  2reuswapdc  2968  reuind  2969  2rmorex  2970  sbccomlem  3064  elunirab  3853  rexxfrd  4499  opeliunxp  4719  elres  4983  resoprab  6022  ov6g  6065  opabex3d  6187  opabex3  6188  xpassen  6898  distrnqg  7471  distrnq0  7543  rexuz2  9672  2clim  11483  bitsmod  12138  issubrg  13853  isbasis2g  14365  tgval2  14371