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

Theorem an12 535
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 264 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
21anbi1i 453 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
3 anass 398 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
4 anass 398 . 2 (((𝜓𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
52, 3, 43bitr3i 209 1 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  an32  536  an13  537  an12s  539  an4  560  ceqsrexv  2789  rmoan  2857  2reuswapdc  2861  reuind  2862  2rmorex  2863  sbccomlem  2955  elunirab  3719  rexxfrd  4354  opeliunxp  4564  elres  4825  resoprab  5835  ov6g  5876  opabex3d  5987  opabex3  5988  xpassen  6692  distrnqg  7163  distrnq0  7235  rexuz2  9344  2clim  11038  isbasis2g  12139  tgval2  12147
  Copyright terms: Public domain W3C validator