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  651  ancom1s  654  xpord2pred  8088  infsupprpr  9412  muladdmod  13865  fi1uzind  14460  prmgapprmolem  17023  c0snmhm  20434  mat1dimcrng  22452  dmatcrng  22477  cramerlem1  22662  cramer  22666  pmatcollpwscmatlem2  22765  uhgr3cyclex  30267  3cyclfrgrrn  30371  frgrreggt1  30478  grpoidinvlem3  30592  atomli  32468  lfuhgr3  35318  cusgredgex  35320  satfun  35609  elnanelprv  35627  arg-ax  36614  bj-prmoore  37443  cnambfre  38003  prter1  39339  prjspersym  43054  rp-oelim2  43754  tfsconcatfv2  43786  tfsconcatrn  43788  oaun3lem2  43821  mnuop3d  44716  eliuniincex  45557  eliincex  45558  dvdsn1add  46385  fourierdlem42  46595  fourierdlem80  46632  etransclem38  46718  modlt0b  47829  prprelprb  47989  reupr  47994  reuopreuprim  47998  gbegt5  48249  uhgrimedg  48379  clnbgrgrim  48422  pgrpgt2nabl  48854