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  5577  eqfnfv3  5734  respreima  5763  fsn  5807  fliftcnv  5919  isoini  5942  spc2ed  6379  brtpos2  6397  tpostpos  6410  tposmpo  6427  nnaord  6655  pmex  6800  elpmg  6811  mapval2  6825  mapsnen  6964  map1  6965  xpsnen  6980  xpcomco  6985  elfi2  7139  supmoti  7160  cnvti  7186  2omotaplemap  7443  elni2  7501  enq0enq  7618  prltlu  7674  prnmaxl  7675  prnminu  7676  nqprrnd  7730  ltpopr  7782  letri3  8227  lesub0  8626  creur  9106  xrletri3  10000  iooneg  10184  iccneg  10185  elfzuzb  10215  fzrev  10280  redivap  11385  imdivap  11392  rersqreu  11539  lenegsq  11606  climrecvg1n  11859  fisumcom2  11949  fsumcom  11950  fprodcom2fi  12137  fprodcom  12138  gcdcom  12494  bezoutlembi  12526  dfgcd2  12535  lcmcom  12586  isprm2  12639  unennn  12968  dfrhm2  14118  issubrng  14163  ntreq0  14806  restopn2  14857  ismet2  15028  blres  15108  metrest  15180  dedekindicclemicc  15306  sincosq3sgn  15502  lgsdi  15716  lgsquadlem3  15758  2lgslem1a  15767