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  1461  exancom  1632  19.29r  1645  19.42h  1711  19.42  1712  eu1  2080  moaneu  2132  moanmo  2133  2eu7  2150  eq2tri  2267  r19.28av  2644  r19.29r  2646  r19.42v  2665  rexcomf  2670  rabswap  2687  euxfr2dc  2965  rmo4  2973  reu8  2976  rmo3f  2977  rmo3  3098  incom  3373  difin2  3443  symdifxor  3447  elif  3591  inuni  4215  eqvinop  4305  uniuni  4516  dtruex  4625  elvvv  4756  brinxp2  4760  dmuni  4907  dfres2  5030  dfima2  5043  imadmrn  5051  imai  5057  cnvxp  5120  cnvcnvsn  5178  mptpreima  5195  rnco  5208  unixpm  5237  ressn  5242  xpcom  5248  fncnv  5359  fununi  5361  imadiflem  5372  fnres  5412  fnopabg  5419  dff1o2  5549  eqfnfv3  5702  respreima  5731  fsn  5775  fliftcnv  5887  isoini  5910  spc2ed  6342  brtpos2  6360  tpostpos  6373  tposmpo  6390  nnaord  6618  pmex  6763  elpmg  6774  mapval2  6788  mapsnen  6927  map1  6928  xpsnen  6941  xpcomco  6946  elfi2  7100  supmoti  7121  cnvti  7147  2omotaplemap  7404  elni2  7462  enq0enq  7579  prltlu  7635  prnmaxl  7636  prnminu  7637  nqprrnd  7691  ltpopr  7743  letri3  8188  lesub0  8587  creur  9067  xrletri3  9961  iooneg  10145  iccneg  10146  elfzuzb  10176  fzrev  10241  redivap  11300  imdivap  11307  rersqreu  11454  lenegsq  11521  climrecvg1n  11774  fisumcom2  11864  fsumcom  11865  fprodcom2fi  12052  fprodcom  12053  gcdcom  12409  bezoutlembi  12441  dfgcd2  12450  lcmcom  12501  isprm2  12554  unennn  12883  dfrhm2  14031  issubrng  14076  ntreq0  14719  restopn2  14770  ismet2  14941  blres  15021  metrest  15093  dedekindicclemicc  15219  sincosq3sgn  15415  lgsdi  15629  lgsquadlem3  15671  2lgslem1a  15680