Theorem pm3.22 463

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  ancom  464  ancom2s  650  ancom1s  653  r19.29r  3167  infsupprpr  9098  fi1uzind  14028  prmgapprmolem  16577  mat1dimcrng  21328  dmatcrng  21353  cramerlem1  21538  cramer  21542  pmatcollpwscmatlem2  21641  uhgr3cyclex  28219  3cyclfrgrrn  28323  frgrreggt1  28430  grpoidinvlem3  28541  atomli  30417  lfuhgr3  32748  cusgredgex  32750  satfun  33040  elnanelprv  33058  xpord2pred  33472  xpord3pred  33478  arg-ax  34291  bj-prmoore  34970  cnambfre  35511  prter1  36579  prjspersym  40095  mnuop3d  41503  eliuniincex  42273  eliincex  42274  dvdsn1add  43098  fourierdlem42  43308  fourierdlem80  43345  etransclem38  43431  prprelprb  44585  reupr  44590  reuopreuprim  44594  gbegt5  44829  c0snmhm  45089  pgrpgt2nabl  45318