Theorem ancom 451

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

Syntax hints:   <-> wb 187   /\ wa 370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 188  df-an 372

This theorem is referenced by:  ancomd  452  ancomst  453  ancomsd  455  pm4.71r  635  pm5.32ri  642  pm5.32rd  644  anbi2ci  700  anbi12ci  702  an12  804  an32  805  an13  806  an42  832  andir  876  dfbi3  901  rbaibOLD  915  rbaibrOLD  916  3anrot  987  3ancoma  989  nancom  1382  nancomOLD  1383  excxor  1406  dfifp6  1426  cador  1506  cadcoma  1510  exancom  1716  19.42v  1823  19.42  2027  sbel2x  2254  moanmo  2328  2eu3  2353  2eu7  2357  2eu8  2358  eq2tri  2490  r19.28v  2962  r19.29r  2964  r19.42v  2983  rexcomf  2988  rabswap  3008  euxfr2  3256  rmo4  3264  reu8  3267  rmo3  3390  incom  3655  difin2  3735  euelss  3760  difin0ss  3861  ssunsn  4157  inuni  4583  reuxfr2d  4641  eqvinop  4702  dfid3  4766  elvvv  4910  brinxp2  4912  dmuni  5060  dfres2  5173  dfima2  5186  imadmrn  5194  imai  5196  asymref2  5233  cnvxp  5270  xpdifid  5281  cnvcnvsn  5329  opswap  5339  mptpreima  5344  rnco  5357  ressn  5388  xpco  5392  wfi  5429  fncnv  5662  fununi  5664  fnres  5707  mptfnf  5714  fnopabg  5716  dff1o2  5833  eqfnfv3  5990  respreima  6021  fsn  6073  f13dfv  6185  fliftcnv  6216  isoini  6241  elrnmpt2res  6421  ndmovcom  6467  uniuni  6611  brtpos2  6984  brtpos  6987  tpostpos  6998  tposmpt2  7015  mpt2curryd  7021  oaord  7253  oeeu  7309  nnaord  7325  pmex  7482  elpmg  7492  mapval2  7506  mapsnen  7651  map1  7652  xpsnen  7659  xpcomco  7665  elfi2  7931  supmo  7969  infmo  8014  cp  8364  dfac5lem1  8555  dfac5lem2  8556  dfac5lem3  8557  dfac2  8562  kmlem3  8583  cdacomen  8612  cf0  8682  cflim3  8693  brdom7disj  8960  brdom6disj  8961  recmulnq  9390  letri3  9720  lesub0  10132  wloglei  10147  mulsuble0b  10478  creur  10604  indstr  11228  xrltlen  11446  xrletri3  11452  qbtwnre  11493  xmulcom  11553  xmulneg1  11556  xmulf  11559  iooneg  11753  iccneg  11754  elfzuzb  11795  fzrev  11859  ssfzoulel  12005  injresinj  12025  xpcogend  13027  rediv  13183  imdiv  13190  lenegsq  13372  o1lo1  13589  fsumcom2  13823  fsumcom  13824  fprodcom2  14026  fprodcom  14027  divalglem10  14371  smueqlem  14452  gcdcom  14472  lcmcom  14545  isprm2  14620  infpn2  14845  imasleval  15435  invsym  15655  dfiso3  15666  subsubc  15746  isffth2  15809  odulatb  16377  oduclatb  16378  posglbmo  16381  resscntz  16973  oppgid  16995  gsumcom  17597  dfrhm2  17933  lsslss  18172  fiidomfld  18520  opsrtoslem1  18695  xrsdsreclb  19003  znleval  19112  gsumcom3  19411  madutpos  19654  fvmptnn04if  19860  ntreq0  20080  restopn2  20180  ist0-3  20348  1stcelcls  20463  txkgen  20654  trfil2  20889  elflim2  20966  flimrest  20985  txflf  21008  fclsrest  21026  tsmssubm  21144  ismet2  21335  blres  21433  metrest  21526  restmetu  21572  xrtgioo  21811  elii1  21950  evthicc2  22398  ovolfcl  22406  ovoliunlem1  22442  dyaddisj  22541  mbfaddlem  22603  itg1climres  22659  mbfi1fseqlem4  22663  iblpos  22737  itgposval  22740  ditgsplit  22803  ellimc3  22821  itgsubst  22988  deg1ldg  23028  sincosq1sgn  23440  sincosq3sgn  23442  cos11  23469  dvdsflsumcom  24104  fsumvma  24128  logfaclbnd  24137  dchrelbas3  24153  lgsdi  24247  lgsquadlem1  24269  lgsquadlem2  24270  lgsquadlem3  24271  istrkg2ld  24495  tgcgr4  24563  mirreu3  24686  hpgcom  24796  colhp  24799  dfcgra2  24858  cusgra3v  25178  trls  25252  trlon  25256  pthon  25291  spthon  25298  3v3e3cycl2  25378  wwlkextinj  25444  clwwlkn2  25489  usg2spthonot0  25603  rusgranumwlkl1  25661  rusgra0edg  25669  eupath2lem2  25692  frg2wot1  25771  frg2woteqm  25773  usg2spot2nb  25779  usgreg2spot  25781  frgrareg  25831  frgraregord013  25832  h2hcau  26618  h2hlm  26619  axhcompl-zf  26637  nmopub  27547  nmfnleub  27564  chrelati  28003  cvexchlem  28007  mdsymlem8  28049  sumdmdii  28054  spc2ed  28092  reuxfr3d  28111  rmo3f  28117  rmo4fOLD  28118  2ndpreima  28278  fpwrelmapffslem  28311  xrofsup  28347  pmtrprfv2  28607  smatrcl  28618  cnvordtrestixx  28715  issgon  28941  eulerpartlemr  29203  eulerpartlemgvv  29205  ballotlem2  29317  sgn3da  29408  bnj257  29508  bnj545  29702  bnj594  29719  coep  30386  dfpo2  30390  dfdm5  30413  dfrn5  30414  elima4  30416  frind  30476  nocvxmin  30573  brtxp  30640  elfix  30663  dffix2  30665  sscoid  30673  brimg  30697  brsuccf  30701  funpartfun  30703  dfrecs2  30710  dfrdg4  30711  cgrcomlr  30758  ofscom  30767  btwnexch  30785  fscgr  30840  bj-dfifc2  31151  bj-eldiag  31598  bj-ccinftydisj  31607  mptsnunlem  31681  topdifinffinlem  31691  wl-cases2-dnf  31764  wl-ax11-lem4  31832  fin2solem  31845  poimirlem4  31858  poimirlem26  31880  poimirlem30  31884  poimirlem32  31886  ftc1anclem6  31936  ftc1anc  31939  heibor1  32056  isdrngo3  32112  isdmn3  32221  an43OLD  32339  prtlem70  32341  prtlem90  32347  lrelat  32499  islshpat  32502  atlrelat1  32806  ishlat2  32838  pmapglb  33254  polval2N  33390  cdlemb3  34092  diblsmopel  34658  dicelval3  34667  diclspsn  34681  fz1eqin  35530  diophrex  35537  fphpd  35578  fzneg  35752  expdioph  35798  dford4  35804  lnr2i  35895  fgraphopab  36007  ifpancor  36027  ifpdfbi  36037  ifpidg  36055  ifpid2g  36057  ifpid1g  36058  ifpim23g  36059  ifp1bi  36066  rp-fakeoranass  36078  relexp0eq  36153  isprm7  36518  uunT1p1  37029  uun132p1  37034  un2122  37038  uun2131p1  37040  uunT12p1  37048  uunT12p2  37049  uunT12p3  37050  uun2221  37061  uun2221p1  37062  uun2221p2  37063  3impdirp1  37064  ancomstVD  37123  icccncfext  37585  dvnmul  37638  dvmptfprodlem  37639  dvnprodlem2  37642  fourierdlem42  37832  fourierdlem42OLD  37833  fourierdlem83  37873  2reu3  38322  2reu7  38325  2reu8  38326  ndmaovcom  38419  usgra2pth0  38941  2zrngnmrid  39222  opeliun2xp  39388  eliunxp2  39389