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  2972  rmoan  3034  2reuswap  3038  reuind  3039  sbccomlem  3116  elunirab  3904  pw1in  4164  eluni1g  4172  insklem  4304  addcass  4415  setconslem4  4734  opeliunxp  4820  elres  4995  dff1o2  5291  dfoprab2  5558  resoprab  5581  ov6g  5600  nmembers1lem1  6268