NFE Home 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  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
  Copyright terms: Public domain W3C validator