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  8808  creur  9291  xrletri3  10216  iooneg  10400  iccneg  10401  elfzuzb  10432  fzrev  10501  redivap  11653  imdivap  11660  rersqreu  11808  lenegsq  11876  climrecvg1n  12130  fisumcom2  12221  fsumcom  12222  fprodcom2fi  12409  fprodcom  12410  gcdcom  12766  bezoutlembi  12798  dfgcd2  12807  lcmcom  12858  isprm2  12911  ballotfilem2  13277  unennn  13337  dfrhm2  14510  issubrng  14556  ntreq0  15282  restopn2  15333  ismet2  15504  blres  15584  metrest  15656  dedekindicclemicc  15782  sincosq3sgn  15979  lgsdi  16254  lgsquadlem3  16296  2lgslem1a  16305  clwwlkn1  16757  clwwlkn2  16760  iseupthf1o  16787  eupth2lem2dc  16798  2alsraln0m  17256