Theorem an12 528

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 262	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2	1	anbi1i 446	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ps /\ ph ) /\ ch ) )
3		anass 393	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
4		anass 393	. 2 |- ( ( ( ps /\ ph ) /\ ch ) <-> ( ps /\ ( ph /\ ch ) ) )
5	2, 3, 4	3bitr3i 208	1 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ps /\ ( ph /\ ch ) ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  an32  529  an13  530  an12s  532  an4  553  ceqsrexv  2747  rmoan  2815  2reuswapdc  2819  reuind  2820  2rmorex  2821  sbccomlem  2913  elunirab  3666  rexxfrd  4285  opeliunxp  4493  elres  4748  resoprab  5741  ov6g  5782  opabex3d  5892  opabex3  5893  xpassen  6546  distrnqg  6946  distrnq0  7018  rexuz2  9069  2clim  10689