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  563  an32  564  an13  565  an42  589  andir  826  rbaib  928  rbaibr  929  ifptru  997  ifpfal  998  3anrot  1009  3ancoma  1011  excxor  1422  xorcom  1432  xordc  1436  xordc1  1437  dfbi3dc  1441  ancomsimp  1485  exancom  1656  19.29r  1669  19.42h  1735  19.42  1736  eu1  2104  moaneu  2156  moanmo  2157  2eu7  2174  eq2tri  2291  r19.28av  2669  r19.29r  2671  r19.42v  2690  rexcomf  2695  rabswap  2712  euxfr2dc  2991  rmo4  2999  reu8  3002  rmo3f  3003  rmo3  3124  incom  3399  difin2  3469  symdifxor  3473  elif  3617  inuni  4245  eqvinop  4335  uniuni  4548  dtruex  4657  elvvv  4789  brinxp2  4793  dmuni  4941  dfres2  5065  dfima2  5078  imadmrn  5086  imai  5092  cnvxp  5155  cnvcnvsn  5213  mptpreima  5230  rnco  5243  unixpm  5272  ressn  5277  xpcom  5283  fncnv  5396  fununi  5398  imadiflem  5409  fnres  5449  fnopabg  5456  dff1o2  5588  eqfnfv3  5746  respreima  5775  fsn  5819  fliftcnv  5936  isoini  5959  spc2ed  6398  brtpos2  6417  tpostpos  6430  tposmpo  6447  nnaord  6677  pmex  6822  elpmg  6833  mapval2  6847  mapsnen  6986  map1  6987  xpsnen  7005  xpcomco  7010  elfi2  7171  supmoti  7192  cnvti  7218  2omotaplemap  7476  elni2  7534  enq0enq  7651  prltlu  7707  prnmaxl  7708  prnminu  7709  nqprrnd  7763  ltpopr  7815  letri3  8260  lesub0  8659  creur  9139  xrletri3  10039  iooneg  10223  iccneg  10224  elfzuzb  10254  fzrev  10319  redivap  11452  imdivap  11459  rersqreu  11606  lenegsq  11673  climrecvg1n  11926  fisumcom2  12017  fsumcom  12018  fprodcom2fi  12205  fprodcom  12206  gcdcom  12562  bezoutlembi  12594  dfgcd2  12603  lcmcom  12654  isprm2  12707  unennn  13036  dfrhm2  14187  issubrng  14232  ntreq0  14875  restopn2  14926  ismet2  15097  blres  15177  metrest  15249  dedekindicclemicc  15375  sincosq3sgn  15571  lgsdi  15785  lgsquadlem3  15827  2lgslem1a  15836  clwwlkn1  16288  clwwlkn2  16291  iseupthf1o  16318  eupth2lem2dc  16329