Theorem pm3.22 464

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 23	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜑))
2	1	ancoms 463	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ancom  465  ancom2s  662  ancom1s  665  xpord2pred  8129  infsupprpr  9454  muladdmod  13939  fi1uzind  14534  prmgapprmolem  17111  c0snmhm  20536  mat1dimcrng  22595  dmatcrng  22620  cramerlem1  22805  cramer  22809  pmatcollpwscmatlem2  22908  uhgr3cyclex  30442  3cyclfrgrrn  30546  frgrreggt1  30653  grpoidinvlem3  30767  atomli  32643  lfuhgr3  35483  cusgredgex  35485  satfun  35774  elnanelprv  35792  arg-ax  36789  bj-prmoore  37617  cnambfre  38179  prter1  39515  prjspersym  43201  rp-oelim2  43897  tfsconcatfv2  43929  tfsconcatrn  43931  oaun3lem2  43964  mnuop3d  44845  eliuniincex  45685  eliincex  45686  dvdsn1add  46511  fourierdlem42  46721  fourierdlem80  46758  etransclem38  46844  modlt0b  47961  prprelprb  48121  reupr  48126  reuopreuprim  48130  gbegt5  48381  uhgrimedg  48511  clnbgrgrim  48554  pgrpgt2nabl  48997