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

Theorem an12 551
 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 454 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
3 anass 399 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
4 anass 399 . 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  552  an13  553  an12s  555  an4  576  ceqsrexv  2820  rmoan  2889  2reuswapdc  2893  reuind  2894  2rmorex  2895  sbccomlem  2988  elunirab  3758  rexxfrd  4393  opeliunxp  4604  elres  4865  resoprab  5877  ov6g  5918  opabex3d  6029  opabex3  6030  xpassen  6734  distrnqg  7242  distrnq0  7314  rexuz2  9426  2clim  11125  isbasis2g  12274  tgval2  12282
 Copyright terms: Public domain W3C validator