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  8075  infsupprpr  9390  muladdmod  13816  fi1uzind  14411  prmgapprmolem  16970  c0snmhm  20379  mat1dimcrng  22390  dmatcrng  22415  cramerlem1  22600  cramer  22604  pmatcollpwscmatlem2  22703  uhgr3cyclex  30157  3cyclfrgrrn  30261  frgrreggt1  30368  grpoidinvlem3  30481  atomli  32357  lfuhgr3  35152  cusgredgex  35154  satfun  35443  elnanelprv  35461  arg-ax  36449  bj-prmoore  37148  cnambfre  37707  prter1  38917  prjspersym  42639  rp-oelim2  43340  tfsconcatfv2  43372  tfsconcatrn  43374  oaun3lem2  43407  mnuop3d  44303  eliuniincex  45145  eliincex  45146  dvdsn1add  45976  fourierdlem42  46186  fourierdlem80  46223  etransclem38  46309  modlt0b  47393  prprelprb  47547  reupr  47552  reuopreuprim  47556  gbegt5  47791  uhgrimedg  47921  clnbgrgrim  47964  pgrpgt2nabl  48396