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

Theorem an12 526
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 262 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
21anbi1i 446 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
3 anass 393 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
4 anass 393 . 2 (((𝜓𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
52, 3, 43bitr3i 208 1 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  an32  527  an13  528  an12s  530  an4  551  ceqsrexv  2735  rmoan  2801  2reuswapdc  2805  reuind  2806  2rmorex  2807  sbccomlem  2899  elunirab  3640  rexxfrd  4249  opeliunxp  4451  elres  4705  resoprab  5676  ov6g  5717  opabex3d  5827  opabex3  5828  xpassen  6476  distrnqg  6849  distrnq0  6921  rexuz2  8964  2clim  10514
  Copyright terms: Public domain W3C validator