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  2656  euxfr2dc  2923  rmo4  2931  reu8  2934  rmo3f  2935  rmo3  3055  incom  3328  difin2  3398  symdifxor  3402  inuni  4156  eqvinop  4244  uniuni  4452  dtruex  4559  elvvv  4690  brinxp2  4694  dmuni  4838  dfres2  4960  dfima2  4973  imadmrn  4981  imai  4985  cnvxp  5048  cnvcnvsn  5106  mptpreima  5123  rnco  5136  unixpm  5165  ressn  5170  xpcom  5176  fncnv  5283  fununi  5285  imadiflem  5296  fnres  5333  fnopabg  5340  dff1o2  5467  eqfnfv3  5616  respreima  5645  fsn  5689  fliftcnv  5796  isoini  5819  spc2ed  6234  brtpos2  6252  tpostpos  6265  tposmpo  6282  nnaord  6510  pmex  6653  elpmg  6664  mapval2  6678  mapsnen  6811  map1  6812  xpsnen  6821  xpcomco  6826  elfi2  6971  supmoti  6992  cnvti  7018  2omotaplemap  7256  elni2  7313  enq0enq  7430  prltlu  7486  prnmaxl  7487  prnminu  7488  nqprrnd  7542  ltpopr  7594  letri3  8038  lesub0  8436  creur  8916  xrletri3  9804  iooneg  9988  iccneg  9989  elfzuzb  10019  fzrev  10084  redivap  10883  imdivap  10890  rersqreu  11037  lenegsq  11104  climrecvg1n  11356  fisumcom2  11446  fsumcom  11447  fprodcom2fi  11634  fprodcom  11635  gcdcom  11974  bezoutlembi  12006  dfgcd2  12015  lcmcom  12064  isprm2  12117  unennn  12398  ntreq0  13635  restopn2  13686  ismet2  13857  blres  13937  metrest  14009  dedekindicclemicc  14113  sincosq3sgn  14252  lgsdi  14441