Theorem pm3.22 464

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 463	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2	1	imp 444	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ancom  465  ancom2s  840  ancom1s  843  fi1uzind  13134  fi1uzindOLD  13140  cshwlen  13396  prmgapprmolem  15603  setsstruct  15727  mat1dimcrng  20102  dmatcrng  20127  cramerlem1  20312  cramer  20316  pmatcollpwscmatlem2  20414  constr3lem4  26175  constr3trllem2  26179  constr3trllem3  26180  clwwlkprop  26298  3vfriswmgra  26532  1to2vfriswmgra  26533  frg2woteq  26587  numclwwlkovfel2  26610  frgrareggt1  26643  grpoidinvlem3  26744  atomli  28625  arg-ax  31585  cnambfre  32628  prter1  33182  eliuniincex  38323  eliincex  38324  dvdsn1add  38829  fourierdlem42  39042  fourierdlem80  39079  etransclem38  39165  gbegt5  40183  uhgr3cyclex  41349  3cyclfrgrrn  41456  av-frgrareggt1  41547  c0snmhm  41705  pgrpgt2nabl  41941