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 ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ancomd  267  ancomsd  269  biancomi  270  biancomd  271  pm4.71r  394  pm5.32rd  455  pm5.32ri  459  anbi2ci  463  anbi12ci  465  bianassc  474  mpan10  478  an12  567  an32  568  an13  569  an42  593  andir  831  rbaib  933  rbaibr  934  ifptru  1002  ifpfal  1003  3anrot  1014  3ancoma  1016  excxor  1427  xorcom  1437  xordc  1441  xordc1  1442  dfbi3dc  1446  ancomsimp  1490  exancom  1661  19.29r  1674  19.42h  1739  19.42  1740  eu1  2111  moaneu  2163  moanmo  2164  2eu7  2181  eq2tri  2298  r19.28av  2687  r19.29r  2689  r19.42v  2708  rexcomf  2713  rabswap  2731  euxfr2dc  3011  rmo4  3019  reu8  3022  rmo3f  3023  rmo3  3144  incom  3421  difin2  3493  symdifxor  3497  elif  3652  inuni  4291  eqvinop  4383  uniuni  4597  dtruex  4706  elvvv  4838  brinxp2  4842  dmuni  4991  dfres2  5115  dfima2  5128  imadmrn  5136  imai  5143  cnvxp  5206  cnvcnvsn  5264  mptpreima  5281  rnco  5294  unixpm  5323  ressn  5328  xpcom  5334  fncnv  5447  fununi  5449  imadiflem  5460  fnres  5500  fnopabg  5507  dff1o2  5644  eqfnfv3  5808  respreima  5836  fsn  5880  fliftcnv  6001  isoini  6024  spc2ed  6469  brtpos2  6522  tpostpos  6535  tposmpo  6552  nnaord  6782  pmex  6927  elpmg  6938  mapval2  6959  mapsnend  7099  mapsnen  7100  map1  7101  xpsnen  7119  xpcomco  7124  elfi2  7306  supmoti  7333  cnvti  7359  2omotaplemap  7623  elni2  7681  enq0enq  7798  prltlu  7854  prnmaxl  7855  prnminu  7856  nqprrnd  7910  ltpopr  7962  letri3  8406  lesub0  8807  creur  9289  xrletri3  10206  iooneg  10390  iccneg  10391  elfzuzb  10422  fzrev  10491  redivap  11639  imdivap  11646  rersqreu  11794  lenegsq  11861  climrecvg1n  12114  fisumcom2  12205  fsumcom  12206  fprodcom2fi  12393  fprodcom  12394  gcdcom  12750  bezoutlembi  12782  dfgcd2  12791  lcmcom  12842  isprm2  12895  ballotfilem2  13228  unennn  13288  dfrhm2  14461  issubrng  14507  ntreq0  15233  restopn2  15284  ismet2  15455  blres  15535  metrest  15607  dedekindicclemicc  15733  sincosq3sgn  15929  lgsdi  16156  lgsquadlem3  16198  2lgslem1a  16207  clwwlkn1  16659  clwwlkn2  16662  iseupthf1o  16689  eupth2lem2dc  16700  2alsraln0m  17158