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  xpord2pred  8087  infsupprpr  9409  muladdmod  13835  fi1uzind  14430  prmgapprmolem  16989  c0snmhm  20399  mat1dimcrng  22421  dmatcrng  22446  cramerlem1  22631  cramer  22635  pmatcollpwscmatlem2  22734  uhgr3cyclex  30257  3cyclfrgrrn  30361  frgrreggt1  30468  grpoidinvlem3  30581  atomli  32457  lfuhgr3  35314  cusgredgex  35316  satfun  35605  elnanelprv  35623  arg-ax  36610  bj-prmoore  37316  cnambfre  37865  prter1  39135  prjspersym  42846  rp-oelim2  43546  tfsconcatfv2  43578  tfsconcatrn  43580  oaun3lem2  43613  mnuop3d  44508  eliuniincex  45349  eliincex  45350  dvdsn1add  46179  fourierdlem42  46389  fourierdlem80  46426  etransclem38  46512  modlt0b  47605  prprelprb  47759  reupr  47764  reuopreuprim  47768  gbegt5  48003  uhgrimedg  48133  clnbgrgrim  48176  pgrpgt2nabl  48608