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  3116  xpord2pred  8171  infsupprpr  9545  muladdmod  13954  fi1uzind  14547  prmgapprmolem  17100  c0snmhm  20464  mat1dimcrng  22484  dmatcrng  22509  cramerlem1  22694  cramer  22698  pmatcollpwscmatlem2  22797  uhgr3cyclex  30202  3cyclfrgrrn  30306  frgrreggt1  30413  grpoidinvlem3  30526  atomli  32402  lfuhgr3  35126  cusgredgex  35128  satfun  35417  elnanelprv  35435  arg-ax  36418  bj-prmoore  37117  cnambfre  37676  prter1  38881  prjspersym  42622  rp-oelim2  43326  tfsconcatfv2  43358  tfsconcatrn  43360  oaun3lem2  43393  mnuop3d  44295  eliuniincex  45119  eliincex  45120  dvdsn1add  45959  fourierdlem42  46169  fourierdlem80  46206  etransclem38  46292  prprelprb  47509  reupr  47514  reuopreuprim  47518  gbegt5  47753  clnbgrgrim  47907  pgrpgt2nabl  48287