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  29435  3cyclfrgrrn  29539  frgrreggt1  29646  grpoidinvlem3  29759  atomli  31635  lfuhgr3  34110  cusgredgex  34112  satfun  34402  elnanelprv  34420  arg-ax  35301  bj-prmoore  35996  cnambfre  36536  prter1  37749  prjspersym  41349  rp-oelim2  42058  tfsconcatfv2  42090  tfsconcatrn  42092  oaun3lem2  42125  mnuop3d  43030  eliuniincex  43798  eliincex  43799  dvdsn1add  44655  fourierdlem42  44865  fourierdlem80  44902  etransclem38  44988  prprelprb  46185  reupr  46190  reuopreuprim  46194  gbegt5  46429  c0snmhm  46714  pgrpgt2nabl  47042