MPE Home 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  1089  indifdir  4257  inrab2  4273  reupick  4284  difxp  6014  imadif  6431  respreima  6828  dff1o6  7023  dfoprab2  7201  f11o  7637  xpassen  8599  dfac5lem1  9537  kmlem3  9566  qbtwnre  12580  elioomnf  12820  modfsummod  15137  pcqcl  16181  tosso  17634  subgdmdprd  19085  opsrtoslem1  20192  pjfval2  20781  fvmptnn04if  21385  cmpcov2  21926  tx1cn  22145  tgphaus  22652  isms2  22987  elcncf1di  23430  elii1  23466  isclmp  23628  dvreslem  24434  dvdsflsumcom  25692  upgr2wlk  27377  upgrtrls  27410  upgristrl  27411  fusgr2wsp2nb  28040  cvnbtwn3  29992  ordtconnlem1  31066  1stmbfm  31417  eulerpartlemn  31538  ballotlem2  31645  reprinrn  31788  reprdifc  31797  cusgr3cyclex  32280  dfon3  33250  brsuccf  33299  brsegle2  33467  bj-restn0b  34276  bj-opelidb1  34337  matunitlindflem2  34770  poimirlem25  34798  bddiblnc  34843  ftc1anc  34856  prtlem17  35892  lcvnbtwn3  36044  cvrnbtwn3  36292  islpln5  36551  islvol5  36595  lhpexle3  37028  dibelval3  38163  dihglb2  38358  pm11.6  40601  stoweidlem17  42179  smfsuplem1  42962
  Copyright terms: Public domain W3C validator