Theorem ancom 264

Description: Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.)

Assertion

Ref	Expression
ancom	|- ( ( ph /\ ps ) <-> ( ps /\ ph ) )

Proof of Theorem ancom

Step	Hyp	Ref	Expression
1		pm3.22 263	. 2 |- ( ( ph /\ ps ) -> ( ps /\ ph ) )
2		pm3.22 263	. 2 |- ( ( ps /\ ph ) -> ( ph /\ ps ) )
3	1, 2	impbii 125	1 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ancomd  265  ancomsd  267  biancomi  268  biancomd  269  pm4.71r  388  pm5.32rd  447  pm5.32ri  451  anbi2ci  455  anbi12ci  457  mpan10  466  an12  551  an32  552  an13  553  an42  577  andir  809  rbaib  907  rbaibr  908  3anrot  968  3ancoma  970  excxor  1357  xorcom  1367  xordc  1371  xordc1  1372  dfbi3dc  1376  ancomsimp  1417  exancom  1588  19.29r  1601  19.42h  1666  19.42  1667  eu1  2025  moaneu  2076  moanmo  2077  2eu7  2094  eq2tri  2200  r19.28av  2571  r19.29r  2573  r19.42v  2591  rexcomf  2596  rabswap  2612  euxfr2dc  2873  rmo4  2881  reu8  2884  rmo3f  2885  rmo3  3004  incom  3273  difin2  3343  symdifxor  3347  inuni  4088  eqvinop  4173  uniuni  4380  dtruex  4482  elvvv  4610  brinxp2  4614  dmuni  4757  dfres2  4879  dfima2  4891  imadmrn  4899  imai  4903  cnvxp  4965  cnvcnvsn  5023  mptpreima  5040  rnco  5053  unixpm  5082  ressn  5087  xpcom  5093  fncnv  5197  fununi  5199  imadiflem  5210  fnres  5247  fnopabg  5254  dff1o2  5380  eqfnfv3  5528  respreima  5556  fsn  5600  fliftcnv  5704  isoini  5727  spc2ed  6138  brtpos2  6156  tpostpos  6169  tposmpo  6186  nnaord  6413  pmex  6555  elpmg  6566  mapval2  6580  mapsnen  6713  map1  6714  xpsnen  6723  xpcomco  6728  elfi2  6868  supmoti  6888  cnvti  6914  elni2  7146  enq0enq  7263  prltlu  7319  prnmaxl  7320  prnminu  7321  nqprrnd  7375  ltpopr  7427  letri3  7869  lesub0  8265  creur  8741  xrletri3  9618  iooneg  9801  iccneg  9802  elfzuzb  9831  fzrev  9895  redivap  10678  imdivap  10685  rersqreu  10832  lenegsq  10899  climrecvg1n  11149  fisumcom2  11239  fsumcom  11240  gcdcom  11698  bezoutlembi  11729  dfgcd2  11738  lcmcom  11781  isprm2  11834  unennn  11946  ntreq0  12340  restopn2  12391  ismet2  12562  blres  12642  metrest  12714  dedekindicclemicc  12818  sincosq3sgn  12957