Theorem pm3.22 465

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		pm3.21 464	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2	1	imp 445	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 384

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 386

This theorem is referenced by:  ancom  466  ancom2s  844  ancom1s  847  fi1uzind  13279  fi1uzindOLD  13285  cshwlen  13545  prmgapprmolem  15765  setsstructOLD  15899  mat1dimcrng  20283  dmatcrng  20308  cramerlem1  20493  cramer  20497  pmatcollpwscmatlem2  20595  uhgr3cyclex  27042  3cyclfrgrrn  27150  frgrreggt1  27251  grpoidinvlem3  27360  atomli  29241  arg-ax  32415  cnambfre  33458  prter1  34164  eliuniincex  39292  eliincex  39293  dvdsn1add  40154  fourierdlem42  40366  fourierdlem80  40403  etransclem38  40489  gbegt5  41649  c0snmhm  41915  pgrpgt2nabl  42147