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

Theorem an32 636
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 anass 460 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12 635 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
3 ancom 452 . 2 ((𝜓 ∧ (𝜑𝜒)) ↔ ((𝜑𝜒) ∧ 𝜓))
41, 2, 33bitri 288 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  an32s  642  3anan32  1118  indifdir  4050  inrab2  4066  reupick  4077  difxp  5743  imadif  6153  respreima  6536  dff1o6  6725  dfoprab2  6901  f11o  7328  mpt2curryd  7600  xpassen  8263  dfac5lem1  9199  kmlem3  9229  qbtwnre  12235  elioomnf  12474  modfsummod  14813  pcqcl  15843  tosso  17305  subgdmdprd  18703  opsrtoslem1  19760  pjfval2  20332  fvmptnn04if  20936  cmpcov2  21476  tx1cn  21695  tgphaus  22202  isms2  22537  elcncf1di  22980  elii1  23016  isclmp  23178  dvreslem  23967  dvdsflsumcom  25208  upgr2wlk  26858  upgrtrls  26893  upgristrl  26894  fusgr2wsp2nb  27617  cvnbtwn3  29606  ordtconnlem1  30420  1stmbfm  30772  eulerpartlemn  30893  ballotlem2  31001  reprinrn  31150  reprdifc  31159  dfon3  32446  brsuccf  32495  brsegle2  32663  bj-restn0b  33475  matunitlindflem2  33833  poimirlem25  33861  bddiblnc  33906  ftc1anc  33919  prtlem17  34835  lcvnbtwn3  34987  cvrnbtwn3  35235  islpln5  35494  islvol5  35538  lhpexle3  35971  dibelval3  37106  dihglb2  37301  pm11.6  39269  stoweidlem17  40874  smfsuplem1  41660
  Copyright terms: Public domain W3C validator