Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  an32 Structured version   Visualization version   GIF version

Theorem an32 642
 Description: A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
Assertion
Ref Expression
an32 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))

Proof of Theorem an32
StepHypRef Expression
1 an21 640 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
21biancomi 463 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   ∧ wa 396 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 208  df-an 397 This theorem is referenced by:  an32s  648  3anan32  1091  indifdir  4263  inrab2  4279  reupick  4290  difxp  6018  imadif  6434  respreima  6831  dff1o6  7029  dfoprab2  7207  f11o  7642  xpassen  8603  dfac5lem1  9541  kmlem3  9570  qbtwnre  12585  elioomnf  12825  modfsummod  15141  pcqcl  16185  tosso  17638  subgdmdprd  19078  opsrtoslem1  20184  pjfval2  20771  fvmptnn04if  21375  cmpcov2  21916  tx1cn  22135  tgphaus  22642  isms2  22977  elcncf1di  23420  elii1  23456  isclmp  23618  dvreslem  24424  dvdsflsumcom  25681  upgr2wlk  27366  upgrtrls  27399  upgristrl  27400  fusgr2wsp2nb  28029  cvnbtwn3  29981  ordtconnlem1  31055  1stmbfm  31406  eulerpartlemn  31527  ballotlem2  31634  reprinrn  31777  reprdifc  31786  cusgr3cyclex  32269  dfon3  33239  brsuccf  33288  brsegle2  33456  bj-restn0b  34265  bj-opelidb1  34326  matunitlindflem2  34758  poimirlem25  34786  bddiblnc  34831  ftc1anc  34844  prtlem17  35881  lcvnbtwn3  36033  cvrnbtwn3  36281  islpln5  36540  islvol5  36584  lhpexle3  37017  dibelval3  38152  dihglb2  38347  pm11.6  40591  stoweidlem17  42170  smfsuplem1  42953
 Copyright terms: Public domain W3C validator