Theorem ancom 264

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 263	. 2 |- ( ( ph /\ ps ) -> ( ps /\ ph ) )
2		pm3.22 263	. 2 |- ( ( ps /\ ph ) -> ( ph /\ ps ) )
3	1, 2	impbii 125	1 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ancomd  265  ancomsd  267  biancomi  268  biancomd  269  pm4.71r  387  pm5.32rd  446  pm5.32ri  450  anbi2ci  454  anbi12ci  456  mpan10  465  an12  550  an32  551  an13  552  an42  576  andir  808  rbaib  906  rbaibr  907  3anrot  967  3ancoma  969  excxor  1356  xorcom  1366  xordc  1370  xordc1  1371  dfbi3dc  1375  ancomsimp  1416  exancom  1587  19.29r  1600  19.42h  1665  19.42  1666  eu1  2024  moaneu  2075  moanmo  2076  2eu7  2093  eq2tri  2199  r19.28av  2568  r19.29r  2570  r19.42v  2588  rexcomf  2593  rabswap  2609  euxfr2dc  2869  rmo4  2877  reu8  2880  rmo3f  2881  rmo3  3000  incom  3268  difin2  3338  symdifxor  3342  inuni  4080  eqvinop  4165  uniuni  4372  dtruex  4474  elvvv  4602  brinxp2  4606  dmuni  4749  dfres2  4871  dfima2  4883  imadmrn  4891  imai  4895  cnvxp  4957  cnvcnvsn  5015  mptpreima  5032  rnco  5045  unixpm  5074  ressn  5079  xpcom  5085  fncnv  5189  fununi  5191  imadiflem  5202  fnres  5239  fnopabg  5246  dff1o2  5372  eqfnfv3  5520  respreima  5548  fsn  5592  fliftcnv  5696  isoini  5719  spc2ed  6130  brtpos2  6148  tpostpos  6161  tposmpo  6178  nnaord  6405  pmex  6547  elpmg  6558  mapval2  6572  mapsnen  6705  map1  6706  xpsnen  6715  xpcomco  6720  elfi2  6860  supmoti  6880  cnvti  6906  elni2  7122  enq0enq  7239  prltlu  7295  prnmaxl  7296  prnminu  7297  nqprrnd  7351  ltpopr  7403  letri3  7845  lesub0  8241  creur  8717  xrletri3  9588  iooneg  9771  iccneg  9772  elfzuzb  9800  fzrev  9864  redivap  10646  imdivap  10653  rersqreu  10800  lenegsq  10867  climrecvg1n  11117  fisumcom2  11207  fsumcom  11208  gcdcom  11662  bezoutlembi  11693  dfgcd2  11702  lcmcom  11745  isprm2  11798  unennn  11910  ntreq0  12301  restopn2  12352  ismet2  12523  blres  12603  metrest  12675  dedekindicclemicc  12779  sincosq3sgn  12909