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  3255  infsupprpr  8954  fi1uzind  13845  prmgapprmolem  16380  mat1dimcrng  21069  dmatcrng  21094  cramerlem1  21279  cramer  21283  pmatcollpwscmatlem2  21381  uhgr3cyclex  27945  3cyclfrgrrn  28049  frgrreggt1  28156  grpoidinvlem3  28267  atomli  30143  lfuhgr3  32373  cusgredgex  32375  satfun  32665  elnanelprv  32683  arg-ax  33771  bj-prmoore  34423  cnambfre  34974  prter1  36047  prjspersym  39349  mnuop3d  40697  eliuniincex  41465  eliincex  41466  dvdsn1add  42314  fourierdlem42  42524  fourierdlem80  42561  etransclem38  42647  prprelprb  43764  reupr  43769  reuopreuprim  43773  gbegt5  44011  c0snmhm  44271  pgrpgt2nabl  44499