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  7334  cnvti  7360  2omotaplemap  7624  elni2  7682  enq0enq  7799  prltlu  7855  prnmaxl  7856  prnminu  7857  nqprrnd  7911  ltpopr  7963  letri3  8407  lesub0  8809  creur  9292  xrletri3  10217  iooneg  10401  iccneg  10402  elfzuzb  10433  fzrev  10502  redivap  11655  imdivap  11662  rersqreu  11810  lenegsq  11878  climrecvg1n  12133  fisumcom2  12224  fsumcom  12225  fprodcom2fi  12412  fprodcom  12413  gcdcom  12769  bezoutlembi  12801  dfgcd2  12810  lcmcom  12861  isprm2  12914  ballotfilem2  13280  unennn  13340  dfrhm2  14545  issubrng  14591  ntreq0  15324  restopn2  15375  ismet2  15546  blres  15626  metrest  15698  dedekindicclemicc  15824  sincosq3sgn  16021  bpos  16281  lgsdi  16322  lgsquadlem3  16364  2lgslem1a  16373  clwwlkn1  16825  clwwlkn2  16828  iseupthf1o  16855  eupth2lem2dc  16866  2alsraln0m  17325