Theorem pm3.22 461

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ancom  462  ancom2s  649  ancom1s  652  r19.29rOLD  3118  xpord2pred  8131  infsupprpr  9499  fi1uzind  14458  prmgapprmolem  16994  mat1dimcrng  21979  dmatcrng  22004  cramerlem1  22189  cramer  22193  pmatcollpwscmatlem2  22292  uhgr3cyclex  29466  3cyclfrgrrn  29570  frgrreggt1  29677  grpoidinvlem3  29790  atomli  31666  lfuhgr3  34141  cusgredgex  34143  satfun  34433  elnanelprv  34451  gg-cncrng  35231  arg-ax  35349  bj-prmoore  36044  cnambfre  36584  prter1  37797  prjspersym  41397  rp-oelim2  42106  tfsconcatfv2  42138  tfsconcatrn  42140  oaun3lem2  42173  mnuop3d  43078  eliuniincex  43846  eliincex  43847  dvdsn1add  44703  fourierdlem42  44913  fourierdlem80  44950  etransclem38  45036  prprelprb  46233  reupr  46238  reuopreuprim  46242  gbegt5  46477  c0snmhm  46762  pgrpgt2nabl  47090