Theorem pm3.22 459

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ancom  460  ancom2s  649  ancom1s  652  r19.29rOLD  3123  xpord2pred  8186  infsupprpr  9573  fi1uzind  14556  prmgapprmolem  17108  c0snmhm  20489  mat1dimcrng  22504  dmatcrng  22529  cramerlem1  22714  cramer  22718  pmatcollpwscmatlem2  22817  uhgr3cyclex  30214  3cyclfrgrrn  30318  frgrreggt1  30425  grpoidinvlem3  30538  atomli  32414  lfuhgr3  35087  cusgredgex  35089  satfun  35379  elnanelprv  35397  arg-ax  36382  bj-prmoore  37081  cnambfre  37628  prter1  38835  prjspersym  42562  rp-oelim2  43270  tfsconcatfv2  43302  tfsconcatrn  43304  oaun3lem2  43337  mnuop3d  44240  eliuniincex  45011  eliincex  45012  dvdsn1add  45860  fourierdlem42  46070  fourierdlem80  46107  etransclem38  46193  prprelprb  47391  reupr  47396  reuopreuprim  47400  gbegt5  47635  clnbgrgrim  47786  pgrpgt2nabl  48091