Theorem an12 772

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

Syntax hints:   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  an32  773  an13  774  an12s  776  an4  797  ceqsrexv  2973  rmoan  3035  2reuswap  3039  reuind  3040  sbccomlem  3117  elunirab  3905  pw1in  4165  eluni1g  4173  insklem  4305  addcass  4416  setconslem4  4735  opeliunxp  4821  elres  4996  dff1o2  5292  dfoprab2  5559  resoprab  5582  ov6g  5601  nmembers1lem1  6269