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  3097  xpord2pred  8124  infsupprpr  9457  muladdmod  13877  fi1uzind  14472  prmgapprmolem  17032  c0snmhm  20372  mat1dimcrng  22364  dmatcrng  22389  cramerlem1  22574  cramer  22578  pmatcollpwscmatlem2  22677  uhgr3cyclex  30111  3cyclfrgrrn  30215  frgrreggt1  30322  grpoidinvlem3  30435  atomli  32311  lfuhgr3  35107  cusgredgex  35109  satfun  35398  elnanelprv  35416  arg-ax  36404  bj-prmoore  37103  cnambfre  37662  prter1  38872  prjspersym  42595  rp-oelim2  43297  tfsconcatfv2  43329  tfsconcatrn  43331  oaun3lem2  43364  mnuop3d  44260  eliuniincex  45103  eliincex  45104  dvdsn1add  45937  fourierdlem42  46147  fourierdlem80  46184  etransclem38  46270  modlt0b  47364  prprelprb  47518  reupr  47523  reuopreuprim  47527  gbegt5  47762  uhgrimedg  47891  clnbgrgrim  47934  pgrpgt2nabl  48354