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

Theorem an32 834
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 678 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12 833 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
3 ancom 464 . 2 ((𝜓 ∧ (𝜑𝜒)) ↔ ((𝜑𝜒) ∧ 𝜓))
41, 2, 33bitri 284 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  an32s  841  3anan32  1042  indifdir  3841  inrab2  3858  reupick  3869  difxp  5462  resco  5541  imadif  5872  respreima  6236  dff1o6  6408  dfoprab2  6576  f11o  6998  mpt2curryd  7259  xpassen  7916  dfac5lem1  8806  kmlem3  8834  qbtwnre  11865  elioomnf  12097  modfsummod  14315  pcqcl  15347  tosso  16807  subgdmdprd  18204  opsrtoslem1  19253  pjfval2  19819  fvmptnn04if  20420  cmpcov2  20950  tx1cn  21169  tgphaus  21677  isms2  22012  elcncf1di  22453  elii1  22489  isclmp  22652  dvreslem  23423  dvdsflsumcom  24658  is2wlk  25888  cvnbtwn3  28324  ordtconlem1  29091  1stmbfm  29442  eulerpartlemn  29563  ballotlem2  29670  dfon3  30962  brsuccf  31011  brsegle2  31179  bj-restn0b  32008  matunitlindflem2  32359  poimirlem25  32387  bddiblnc  32433  ftc1anc  32446  prtlem17  32962  lcvnbtwn3  33116  cvrnbtwn3  33364  islpln5  33622  islvol5  33666  lhpexle3  34099  dibelval3  35237  dihglb2  35432  pm11.6  37397  stoweidlem17  38693  upgr2wlk  40857  upgrtrls  40890  upgristrl  40891
  Copyright terms: Public domain W3C validator