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  819  rbaib  921  rbaibr  922  3anrot  983  3ancoma  985  excxor  1378  xorcom  1388  xordc  1392  xordc1  1393  dfbi3dc  1397  ancomsimp  1440  exancom  1608  19.29r  1621  19.42h  1687  19.42  1688  eu1  2051  moaneu  2102  moanmo  2103  2eu7  2120  eq2tri  2237  r19.28av  2613  r19.29r  2615  r19.42v  2634  rexcomf  2639  rabswap  2655  euxfr2dc  2922  rmo4  2930  reu8  2933  rmo3f  2934  rmo3  3054  incom  3327  difin2  3397  symdifxor  3401  inuni  4155  eqvinop  4243  uniuni  4451  dtruex  4558  elvvv  4689  brinxp2  4693  dmuni  4837  dfres2  4959  dfima2  4972  imadmrn  4980  imai  4984  cnvxp  5047  cnvcnvsn  5105  mptpreima  5122  rnco  5135  unixpm  5164  ressn  5169  xpcom  5175  fncnv  5282  fununi  5284  imadiflem  5295  fnres  5332  fnopabg  5339  dff1o2  5466  eqfnfv3  5615  respreima  5644  fsn  5688  fliftcnv  5795  isoini  5818  spc2ed  6233  brtpos2  6251  tpostpos  6264  tposmpo  6281  nnaord  6509  pmex  6652  elpmg  6663  mapval2  6677  mapsnen  6810  map1  6811  xpsnen  6820  xpcomco  6825  elfi2  6970  supmoti  6991  cnvti  7017  2omotaplemap  7255  elni2  7312  enq0enq  7429  prltlu  7485  prnmaxl  7486  prnminu  7487  nqprrnd  7541  ltpopr  7593  letri3  8037  lesub0  8435  creur  8915  xrletri3  9803  iooneg  9987  iccneg  9988  elfzuzb  10018  fzrev  10083  redivap  10882  imdivap  10889  rersqreu  11036  lenegsq  11103  climrecvg1n  11355  fisumcom2  11445  fsumcom  11446  fprodcom2fi  11633  fprodcom  11634  gcdcom  11973  bezoutlembi  12005  dfgcd2  12014  lcmcom  12063  isprm2  12116  unennn  12397  ntreq0  13602  restopn2  13653  ismet2  13824  blres  13904  metrest  13976  dedekindicclemicc  14080  sincosq3sgn  14219  lgsdi  14408