Theorem pm3.22 447

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

Syntax hints:   → wi 4   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  ancom  448  ancom2s  629  ancom1s  632  fi1uzind  13481  cshwlen  13754  prmgapprmolem  15972  setsstructOLD  16106  mat1dimcrng  20501  dmatcrng  20526  cramerlem1  20713  cramer  20717  pmatcollpwscmatlem2  20815  uhgr3cyclex  27362  3cyclfrgrrn  27468  frgrreggt1  27592  grpoidinvlem3  27700  atomli  29581  arg-ax  32752  cnambfre  33789  prter1  34685  eliuniincex  39811  eliincex  39812  dvdsn1add  40667  fourierdlem42  40878  fourierdlem80  40915  etransclem38  41001  gbegt5  42172  c0snmhm  42438  pgrpgt2nabl  42670