Theorem ancom 266

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 265	. 2 |- ( ( ph /\ ps ) -> ( ps /\ ph ) )
2		pm3.22 265	. 2 |- ( ( ps /\ ph ) -> ( ph /\ ps ) )
3	1, 2	impbii 126	1 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ancomd  267  ancomsd  269  biancomi  270  biancomd  271  pm4.71r  390  pm5.32rd  451  pm5.32ri  455  anbi2ci  459  anbi12ci  461  bianassc  470  mpan10  474  an12  561  an32  562  an13  563  an42  587  andir  824  rbaib  926  rbaibr  927  ifptru  995  ifpfal  996  3anrot  1007  3ancoma  1009  excxor  1420  xorcom  1430  xordc  1434  xordc1  1435  dfbi3dc  1439  ancomsimp  1483  exancom  1654  19.29r  1667  19.42h  1733  19.42  1734  eu1  2102  moaneu  2154  moanmo  2155  2eu7  2172  eq2tri  2289  r19.28av  2667  r19.29r  2669  r19.42v  2688  rexcomf  2693  rabswap  2710  euxfr2dc  2988  rmo4  2996  reu8  2999  rmo3f  3000  rmo3  3121  incom  3396  difin2  3466  symdifxor  3470  elif  3614  inuni  4239  eqvinop  4329  uniuni  4542  dtruex  4651  elvvv  4782  brinxp2  4786  dmuni  4933  dfres2  5057  dfima2  5070  imadmrn  5078  imai  5084  cnvxp  5147  cnvcnvsn  5205  mptpreima  5222  rnco  5235  unixpm  5264  ressn  5269  xpcom  5275  fncnv  5387  fununi  5389  imadiflem  5400  fnres  5440  fnopabg  5447  dff1o2  5579  eqfnfv3  5736  respreima  5765  fsn  5809  fliftcnv  5925  isoini  5948  spc2ed  6385  brtpos2  6403  tpostpos  6416  tposmpo  6433  nnaord  6663  pmex  6808  elpmg  6819  mapval2  6833  mapsnen  6972  map1  6973  xpsnen  6988  xpcomco  6993  elfi2  7150  supmoti  7171  cnvti  7197  2omotaplemap  7454  elni2  7512  enq0enq  7629  prltlu  7685  prnmaxl  7686  prnminu  7687  nqprrnd  7741  ltpopr  7793  letri3  8238  lesub0  8637  creur  9117  xrletri3  10012  iooneg  10196  iccneg  10197  elfzuzb  10227  fzrev  10292  redivap  11401  imdivap  11408  rersqreu  11555  lenegsq  11622  climrecvg1n  11875  fisumcom2  11965  fsumcom  11966  fprodcom2fi  12153  fprodcom  12154  gcdcom  12510  bezoutlembi  12542  dfgcd2  12551  lcmcom  12602  isprm2  12655  unennn  12984  dfrhm2  14134  issubrng  14179  ntreq0  14822  restopn2  14873  ismet2  15044  blres  15124  metrest  15196  dedekindicclemicc  15322  sincosq3sgn  15518  lgsdi  15732  lgsquadlem3  15774  2lgslem1a  15783  clwwlkn1  16160  clwwlkn2  16163