Theorem pm3.22 459

Description: Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)

Assertion

Ref	Expression
pm3.22	⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))

Proof of Theorem pm3.22

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜑))
2	1	ancoms 458	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ancom  460  ancom2s  650  ancom1s  653  r19.29rOLD  3098  xpord2pred  8127  infsupprpr  9464  muladdmod  13884  fi1uzind  14479  prmgapprmolem  17039  c0snmhm  20379  mat1dimcrng  22371  dmatcrng  22396  cramerlem1  22581  cramer  22585  pmatcollpwscmatlem2  22684  uhgr3cyclex  30118  3cyclfrgrrn  30222  frgrreggt1  30329  grpoidinvlem3  30442  atomli  32318  lfuhgr3  35114  cusgredgex  35116  satfun  35405  elnanelprv  35423  arg-ax  36411  bj-prmoore  37110  cnambfre  37669  prter1  38879  prjspersym  42602  rp-oelim2  43304  tfsconcatfv2  43336  tfsconcatrn  43338  oaun3lem2  43371  mnuop3d  44267  eliuniincex  45110  eliincex  45111  dvdsn1add  45944  fourierdlem42  46154  fourierdlem80  46191  etransclem38  46277  modlt0b  47368  prprelprb  47522  reupr  47527  reuopreuprim  47531  gbegt5  47766  uhgrimedg  47895  clnbgrgrim  47938  pgrpgt2nabl  48358