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

Theorem an32 645
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 643 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
21biancomi 464 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  an32s  651  3anan32  1098  indifdirOLD  4246  inrab2  4268  reupick  4279  difxp  6117  imadif  6586  respreima  7017  dff1o6  7222  dfoprab2  7416  f11o  7880  xpassen  9011  dfac5lem1  10060  kmlem3  10089  qbtwnre  13119  elioomnf  13362  modfsummod  15680  pcqcl  16729  tosso  18309  subgdmdprd  19814  pjfval2  21118  opsrtoslem1  21465  fvmptnn04if  22201  cmpcov2  22744  tx1cn  22963  tgphaus  23471  isms2  23806  elcncf1di  24261  elii1  24301  isclmp  24463  bddiblnc  25209  dvreslem  25276  dvdsflsumcom  26540  upgr2wlk  28619  upgrtrls  28652  upgristrl  28653  fusgr2wsp2nb  29281  cvnbtwn3  31233  ssmxidllem  32241  ordtconnlem1  32508  1stmbfm  32863  eulerpartlemn  32984  ballotlem2  33091  reprinrn  33234  reprdifc  33243  cusgr3cyclex  33733  dfon3  34480  brsuccf  34529  brsegle2  34697  bj-restn0b  35565  bj-opelidb1  35627  matunitlindflem2  36078  poimirlem25  36106  ftc1anc  36162  disjlem17  37264  prtlem17  37341  lcvnbtwn3  37493  cvrnbtwn3  37741  islpln5  38001  islvol5  38045  lhpexle3  38478  dibelval3  39613  dihglb2  39808  pm11.6  42679  stoweidlem17  44265  smfsuplem1  45059
  Copyright terms: Public domain W3C validator