Theorem pm3.22 465

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ancom  466  ancom2s  663  ancom1s  666  xpord2pred  8146  infsupprpr  9482  muladdmod  14035  fi1uzind  14632  prmgapprmolem  17219  c0snmhm  20673  mat1dimcrng  22772  dmatcrng  22797  cramerlem1  22985  cramer  22989  pmatcollpwscmatlem2  23088  lfuhgr3  29710  uhgr3cyclex  30765  3cyclfrgrrn  30869  frgrreggt1  30976  grpoidinvlem3  31090  atomli  32966  cusgredgex  35875  satfun  36145  elnanelprv  36163  arg-ax  37174  bj-prmoore  38004  cnambfre  38554  prter1  39904  prjspersym  43597  rp-oelim2  44268  tfsconcatfv2  44300  tfsconcatrn  44302  oaun3lem2  44335  mnuop3d  45214  eliuniincex  46067  eliincex  46068  dvdsn1add  46893  fourierdlem42  47103  fourierdlem80  47140  etransclem38  47226  modlt0b  48383  prprelprb  48543  reupr  48548  reuopreuprim  48552  gbegt5  48803  uhgrimedg  48933  clnbgrgrim  48976  pgrpgt2nabl  49422