Theorem pm3.22 464

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ancom  465  ancom2s  662  ancom1s  665  xpord2pred  8142  infsupprpr  9467  muladdmod  13950  fi1uzind  14546  prmgapprmolem  17122  c0snmhm  20546  mat1dimcrng  22615  dmatcrng  22640  cramerlem1  22825  cramer  22829  pmatcollpwscmatlem2  22928  uhgr3cyclex  30511  3cyclfrgrrn  30615  frgrreggt1  30722  grpoidinvlem3  30836  atomli  32712  lfuhgr3  35590  cusgredgex  35592  satfun  35881  elnanelprv  35899  arg-ax  36905  bj-prmoore  37735  cnambfre  38297  prter1  39631  prjspersym  43319  rp-oelim2  44015  tfsconcatfv2  44047  tfsconcatrn  44049  oaun3lem2  44082  mnuop3d  44961  eliuniincex  45807  eliincex  45808  dvdsn1add  46633  fourierdlem42  46843  fourierdlem80  46880  etransclem38  46966  modlt0b  48083  prprelprb  48243  reupr  48248  reuopreuprim  48252  gbegt5  48503  uhgrimedg  48633  clnbgrgrim  48676  pgrpgt2nabl  49123