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  8189  infsupprpr  9525  muladdmod  14082  fi1uzind  14679  prmgapprmolem  17268  c0snmhm  20723  mat1dimcrng  22822  dmatcrng  22847  cramerlem1  23035  cramer  23039  pmatcollpwscmatlem2  23138  lfuhgr3  29758  uhgr3cyclex  30813  3cyclfrgrrn  30917  frgrreggt1  31024  grpoidinvlem3  31138  atomli  33014  cusgredgex  36063  satfun  36343  elnanelprv  36361  arg-ax  37382  bj-prmoore  38227  cnambfre  38778  prter1  40128  prjspersym  43828  rp-oelim2  44502  tfsconcatfv2  44534  tfsconcatrn  44536  oaun3lem2  44569  mnuop3d  45447  eliuniincex  46329  eliincex  46330  dvdsn1add  47154  fourierdlem42  47364  fourierdlem80  47401  etransclem38  47487  modlt0b  48644  prprelprb  48804  reupr  48809  reuopreuprim  48813  gbegt5  49064  uhgrimedg  49194  clnbgrgrim  49237  pgrpgt2nabl  49683