Theorem pm3.22 462

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ancom  463  ancom2s  648  ancom1s  651  r19.29r  3257  infsupprpr  8970  fi1uzind  13858  prmgapprmolem  16399  mat1dimcrng  21088  dmatcrng  21113  cramerlem1  21298  cramer  21302  pmatcollpwscmatlem2  21400  uhgr3cyclex  27963  3cyclfrgrrn  28067  frgrreggt1  28174  grpoidinvlem3  28285  atomli  30161  lfuhgr3  32368  cusgredgex  32370  satfun  32660  elnanelprv  32678  arg-ax  33766  bj-prmoore  34409  cnambfre  34942  prter1  36017  prjspersym  39264  mnuop3d  40614  eliuniincex  41382  eliincex  41383  dvdsn1add  42231  fourierdlem42  42441  fourierdlem80  42478  etransclem38  42564  prprelprb  43686  reupr  43691  reuopreuprim  43695  gbegt5  43933  c0snmhm  44193  pgrpgt2nabl  44421