Theorem an12 556

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 264	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2	1	anbi1i 455	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ps /\ ph ) /\ ch ) )
3		anass 399	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
4		anass 399	. 2 |- ( ( ( ps /\ ph ) /\ ch ) <-> ( ps /\ ( ph /\ ch ) ) )
5	2, 3, 4	3bitr3i 209	1 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ps /\ ( ph /\ ch ) ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an32  557  an13  558  an12s  560  an4  581  ceqsrexv  2860  rmoan  2930  2reuswapdc  2934  reuind  2935  2rmorex  2936  sbccomlem  3029  elunirab  3809  rexxfrd  4448  opeliunxp  4666  elres  4927  resoprab  5949  ov6g  5990  opabex3d  6100  opabex3  6101  xpassen  6808  distrnqg  7349  distrnq0  7421  rexuz2  9540  2clim  11264  isbasis2g  12837  tgval2  12845