New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  an12 GIF version

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 ((φ (ψ χ)) ↔ (ψ (φ χ)))

Proof of Theorem an12
StepHypRef Expression
1 ancom 437 . . 3 ((φ ψ) ↔ (ψ φ))
21anbi1i 676 . 2 (((φ ψ) χ) ↔ ((ψ φ) χ))
3 anass 630 . 2 (((φ ψ) χ) ↔ (φ (ψ χ)))
4 anass 630 . 2 (((ψ φ) χ) ↔ (ψ (φ χ)))
52, 3, 43bitr3i 266 1 ((φ (ψ χ)) ↔ (ψ (φ χ)))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator