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

Theorem an12 561
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 266 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
21anbi1i 458 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
3 anass 401 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
4 anass 401 . 2 (((𝜓𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
52, 3, 43bitr3i 210 1 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  an32  562  an13  563  an12s  565  an4  586  ceqsrexv  2891  rmoan  2961  2reuswapdc  2965  reuind  2966  2rmorex  2967  sbccomlem  3061  elunirab  3849  rexxfrd  4495  opeliunxp  4715  elres  4979  resoprab  6015  ov6g  6058  opabex3d  6175  opabex3  6176  xpassen  6886  distrnqg  7449  distrnq0  7521  rexuz2  9649  2clim  11447  issubrg  13720  isbasis2g  14224  tgval2  14230
  Copyright terms: Public domain W3C validator