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  8150  infsupprpr  9476  muladdmod  13968  fi1uzind  14564  prmgapprmolem  17146  c0snmhm  20578  mat1dimcrng  22671  dmatcrng  22696  cramerlem1  22881  cramer  22885  pmatcollpwscmatlem2  22984  uhgr3cyclex  30570  3cyclfrgrrn  30674  frgrreggt1  30781  grpoidinvlem3  30895  atomli  32771  lfuhgr3  35633  cusgredgex  35635  satfun  35924  elnanelprv  35942  arg-ax  36968  bj-prmoore  37798  cnambfre  38360  prter1  39694  prjspersym  43380  rp-oelim2  44076  tfsconcatfv2  44108  tfsconcatrn  44110  oaun3lem2  44143  mnuop3d  45022  eliuniincex  45868  eliincex  45869  dvdsn1add  46694  fourierdlem42  46904  fourierdlem80  46941  etransclem38  47027  modlt0b  48147  prprelprb  48307  reupr  48312  reuopreuprim  48316  gbegt5  48567  uhgrimedg  48697  clnbgrgrim  48740  pgrpgt2nabl  49187