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  4200  eqvinop  4288  uniuni  4499  dtruex  4608  elvvv  4739  brinxp2  4743  dmuni  4889  dfres2  5012  dfima2  5025  imadmrn  5033  imai  5039  cnvxp  5102  cnvcnvsn  5160  mptpreima  5177  rnco  5190  unixpm  5219  ressn  5224  xpcom  5230  fncnv  5341  fununi  5343  imadiflem  5354  fnres  5394  fnopabg  5401  dff1o2  5529  eqfnfv3  5681  respreima  5710  fsn  5754  fliftcnv  5866  isoini  5889  spc2ed  6321  brtpos2  6339  tpostpos  6352  tposmpo  6369  nnaord  6597  pmex  6742  elpmg  6753  mapval2  6767  mapsnen  6905  map1  6906  xpsnen  6918  xpcomco  6923  elfi2  7076  supmoti  7097  cnvti  7123  2omotaplemap  7371  elni2  7429  enq0enq  7546  prltlu  7602  prnmaxl  7603  prnminu  7604  nqprrnd  7658  ltpopr  7710  letri3  8155  lesub0  8554  creur  9034  xrletri3  9928  iooneg  10112  iccneg  10113  elfzuzb  10143  fzrev  10208  redivap  11218  imdivap  11225  rersqreu  11372  lenegsq  11439  climrecvg1n  11692  fisumcom2  11782  fsumcom  11783  fprodcom2fi  11970  fprodcom  11971  gcdcom  12327  bezoutlembi  12359  dfgcd2  12368  lcmcom  12419  isprm2  12472  unennn  12801  dfrhm2  13949  issubrng  13994  ntreq0  14637  restopn2  14688  ismet2  14859  blres  14939  metrest  15011  dedekindicclemicc  15137  sincosq3sgn  15333  lgsdi  15547  lgsquadlem3  15589  2lgslem1a  15598