Theorem pm3.22 460

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 459	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ancom  461  ancom2s  647  ancom1s  650  r19.29r  3185  infsupprpr  9263  fi1uzind  14211  prmgapprmolem  16762  mat1dimcrng  21626  dmatcrng  21651  cramerlem1  21836  cramer  21840  pmatcollpwscmatlem2  21939  uhgr3cyclex  28546  3cyclfrgrrn  28650  frgrreggt1  28757  grpoidinvlem3  28868  atomli  30744  lfuhgr3  33081  cusgredgex  33083  satfun  33373  elnanelprv  33391  xpord2pred  33792  xpord3pred  33798  arg-ax  34605  bj-prmoore  35286  cnambfre  35825  prter1  36893  prjspersym  40446  mnuop3d  41889  eliuniincex  42659  eliincex  42660  dvdsn1add  43480  fourierdlem42  43690  fourierdlem80  43727  etransclem38  43813  prprelprb  44969  reupr  44974  reuopreuprim  44978  gbegt5  45213  c0snmhm  45473  pgrpgt2nabl  45702