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  3105  xpord2pred  8149  infsupprpr  9523  muladdmod  13935  fi1uzind  14530  prmgapprmolem  17086  c0snmhm  20428  mat1dimcrng  22420  dmatcrng  22445  cramerlem1  22630  cramer  22634  pmatcollpwscmatlem2  22733  uhgr3cyclex  30168  3cyclfrgrrn  30272  frgrreggt1  30379  grpoidinvlem3  30492  atomli  32368  lfuhgr3  35147  cusgredgex  35149  satfun  35438  elnanelprv  35456  arg-ax  36439  bj-prmoore  37138  cnambfre  37697  prter1  38902  prjspersym  42597  rp-oelim2  43299  tfsconcatfv2  43331  tfsconcatrn  43333  oaun3lem2  43366  mnuop3d  44262  eliuniincex  45100  eliincex  45101  dvdsn1add  45935  fourierdlem42  46145  fourierdlem80  46182  etransclem38  46268  prprelprb  47498  reupr  47503  reuopreuprim  47507  gbegt5  47742  uhgrimedg  47871  clnbgrgrim  47914  pgrpgt2nabl  48308