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

Theorem an32 835
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 679 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12 834 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
3 ancom 465 . 2 ((𝜓 ∧ (𝜑𝜒)) ↔ ((𝜑𝜒) ∧ 𝜓))
41, 2, 33bitri 285 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  an32s  842  3anan32  1043  indifdir  3842  inrab2  3859  reupick  3870  difxp  5477  resco  5556  imadif  5887  respreima  6252  dff1o6  6431  dfoprab2  6599  f11o  7021  mpt2curryd  7282  xpassen  7939  dfac5lem1  8829  kmlem3  8857  qbtwnre  11904  elioomnf  12139  modfsummod  14367  pcqcl  15399  tosso  16859  subgdmdprd  18256  opsrtoslem1  19305  pjfval2  19872  fvmptnn04if  20473  cmpcov2  21003  tx1cn  21222  tgphaus  21730  isms2  22065  elcncf1di  22506  elii1  22542  isclmp  22705  dvreslem  23479  dvdsflsumcom  24714  is2wlk  26095  cvnbtwn3  28531  ordtconlem1  29298  1stmbfm  29649  eulerpartlemn  29770  ballotlem2  29877  dfon3  31169  brsuccf  31218  brsegle2  31386  bj-restn0b  32225  matunitlindflem2  32576  poimirlem25  32604  bddiblnc  32650  ftc1anc  32663  prtlem17  33179  lcvnbtwn3  33333  cvrnbtwn3  33581  islpln5  33839  islvol5  33883  lhpexle3  34316  dibelval3  35454  dihglb2  35649  pm11.6  37614  stoweidlem17  38910  upgr2wlk  40876  upgrtrls  40909  upgristrl  40910
  Copyright terms: Public domain W3C validator