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  821  rbaib  923  rbaibr  924  3anrot  986  3ancoma  988  excxor  1398  xorcom  1408  xordc  1412  xordc1  1413  dfbi3dc  1417  ancomsimp  1460  exancom  1631  19.29r  1644  19.42h  1710  19.42  1711  eu1  2079  moaneu  2130  moanmo  2131  2eu7  2148  eq2tri  2265  r19.28av  2642  r19.29r  2644  r19.42v  2663  rexcomf  2668  rabswap  2685  euxfr2dc  2958  rmo4  2966  reu8  2969  rmo3f  2970  rmo3  3090  incom  3365  difin2  3435  symdifxor  3439  inuni  4199  eqvinop  4287  uniuni  4498  dtruex  4607  elvvv  4738  brinxp2  4742  dmuni  4888  dfres2  5011  dfima2  5024  imadmrn  5032  imai  5038  cnvxp  5101  cnvcnvsn  5159  mptpreima  5176  rnco  5189  unixpm  5218  ressn  5223  xpcom  5229  fncnv  5340  fununi  5342  imadiflem  5353  fnres  5392  fnopabg  5399  dff1o2  5527  eqfnfv3  5679  respreima  5708  fsn  5752  fliftcnv  5864  isoini  5887  spc2ed  6319  brtpos2  6337  tpostpos  6350  tposmpo  6367  nnaord  6595  pmex  6740  elpmg  6751  mapval2  6765  mapsnen  6903  map1  6904  xpsnen  6916  xpcomco  6921  elfi2  7074  supmoti  7095  cnvti  7121  2omotaplemap  7369  elni2  7427  enq0enq  7544  prltlu  7600  prnmaxl  7601  prnminu  7602  nqprrnd  7656  ltpopr  7708  letri3  8153  lesub0  8552  creur  9032  xrletri3  9926  iooneg  10110  iccneg  10111  elfzuzb  10141  fzrev  10206  redivap  11185  imdivap  11192  rersqreu  11339  lenegsq  11406  climrecvg1n  11659  fisumcom2  11749  fsumcom  11750  fprodcom2fi  11937  fprodcom  11938  gcdcom  12294  bezoutlembi  12326  dfgcd2  12335  lcmcom  12386  isprm2  12439  unennn  12768  dfrhm2  13916  issubrng  13961  ntreq0  14604  restopn2  14655  ismet2  14826  blres  14906  metrest  14978  dedekindicclemicc  15104  sincosq3sgn  15300  lgsdi  15514  lgsquadlem3  15556  2lgslem1a  15565