ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  an12 GIF version

Theorem an12 503
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 257 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
21anbi1i 439 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
3 anass 387 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
4 anass 387 . 2 (((𝜓𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
52, 3, 43bitr3i 203 1 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  an32  504  an13  505  an12s  507  an4  528  ceqsrexv  2696  rmoan  2761  2reuswapdc  2765  reuind  2766  2rmorex  2767  sbccomlem  2859  elunirab  3620  rexxfrd  4222  opeliunxp  4422  elres  4673  resoprab  5624  ov6g  5665  opabex3d  5775  opabex3  5776  xpassen  6334  distrnqg  6542  distrnq0  6614  rexuz2  8619  2clim  10052
  Copyright terms: Public domain W3C validator