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  8164  infsupprpr  9501  muladdmod  14058  fi1uzind  14655  prmgapprmolem  17244  c0snmhm  20698  mat1dimcrng  22797  dmatcrng  22822  cramerlem1  23010  cramer  23014  pmatcollpwscmatlem2  23113  lfuhgr3  29733  uhgr3cyclex  30788  3cyclfrgrrn  30892  frgrreggt1  30999  grpoidinvlem3  31113  atomli  32989  cusgredgex  35982  satfun  36262  elnanelprv  36280  arg-ax  37296  bj-prmoore  38128  cnambfre  38679  prter1  40029  prjspersym  43728  rp-oelim2  44403  tfsconcatfv2  44435  tfsconcatrn  44437  oaun3lem2  44470  mnuop3d  45348  eliuniincex  46217  eliincex  46218  dvdsn1add  47042  fourierdlem42  47252  fourierdlem80  47289  etransclem38  47375  modlt0b  48532  prprelprb  48692  reupr  48697  reuopreuprim  48701  gbegt5  48952  uhgrimedg  49082  clnbgrgrim  49125  pgrpgt2nabl  49571