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  8081  infsupprpr  9397  muladdmod  13821  fi1uzind  14416  prmgapprmolem  16975  c0snmhm  20383  mat1dimcrng  22393  dmatcrng  22418  cramerlem1  22603  cramer  22607  pmatcollpwscmatlem2  22706  uhgr3cyclex  30164  3cyclfrgrrn  30268  frgrreggt1  30375  grpoidinvlem3  30488  atomli  32364  lfuhgr3  35185  cusgredgex  35187  satfun  35476  elnanelprv  35494  arg-ax  36481  bj-prmoore  37180  cnambfre  37728  prter1  38998  prjspersym  42725  rp-oelim2  43425  tfsconcatfv2  43457  tfsconcatrn  43459  oaun3lem2  43492  mnuop3d  44388  eliuniincex  45230  eliincex  45231  dvdsn1add  46061  fourierdlem42  46271  fourierdlem80  46308  etransclem38  46394  modlt0b  47487  prprelprb  47641  reupr  47646  reuopreuprim  47650  gbegt5  47885  uhgrimedg  48015  clnbgrgrim  48058  pgrpgt2nabl  48490