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  8147  infsupprpr  9480  muladdmod  13980  fi1uzind  14576  prmgapprmolem  17159  c0snmhm  20610  mat1dimcrng  22705  dmatcrng  22730  cramerlem1  22918  cramer  22922  pmatcollpwscmatlem2  23021  lfuhgr3  29615  uhgr3cyclex  30670  3cyclfrgrrn  30774  frgrreggt1  30881  grpoidinvlem3  30995  atomli  32871  cusgredgex  35728  satfun  35998  elnanelprv  36016  arg-ax  37043  bj-prmoore  37873  cnambfre  38425  prter1  39760  prjspersym  43461  rp-oelim2  44157  tfsconcatfv2  44189  tfsconcatrn  44191  oaun3lem2  44224  mnuop3d  45103  eliuniincex  45949  eliincex  45950  dvdsn1add  46775  fourierdlem42  46985  fourierdlem80  47022  etransclem38  47108  modlt0b  48265  prprelprb  48425  reupr  48430  reuopreuprim  48434  gbegt5  48685  uhgrimedg  48815  clnbgrgrim  48858  pgrpgt2nabl  49304