Theorem an12 526

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  527  an13  528  an12s  530  an4  551  ceqsrexv  2726  rmoan  2791  2reuswapdc  2795  reuind  2796  2rmorex  2797  sbccomlem  2889  elunirab  3622  rexxfrd  4221  opeliunxp  4421  elres  4674  resoprab  5628  ov6g  5669  opabex3d  5779  opabex3  5780  xpassen  6374  distrnqg  6639  distrnq0  6711  rexuz2  8750  2clim  10278