Theorem ancom 452

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

Syntax hints:   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  ancomd  453  ancomst  454  ancomsd  456  pm4.71r  636  pm5.32ri  643  pm5.32rd  645  anbi2ci  701  anbi12ci  703  an12  805  an32  806  an13  807  an42  833  andir  878  dfbi3  903  rbaibOLD  917  rbaibrOLD  918  3anrot  989  3ancoma  991  nancom  1386  nancomOLD  1387  excxor  1410  dfifp6  1430  cador  1510  cadcoma  1514  exancom  1721  19.42v  1833  19.42  2051  sbel2x  2287  moanmo  2360  2eu3  2383  2eu7  2387  2eu8  2388  eq2tri  2511  r19.28v  2923  r19.29r  2925  r19.42v  2944  rexcomf  2949  rabswap  2969  euxfr2  3222  rmo4  3230  reu8  3233  rmo3  3357  incom  3624  difin2  3704  euelss  3729  difin0ss  3832  ssunsn  4131  inuni  4564  reuxfr2d  4622  eqvinop  4685  dfid3  4749  elvvv  4893  brinxp2  4895  dmuni  5043  dfres2  5156  dfima2  5169  imadmrn  5177  imai  5179  asymref2  5216  cnvxp  5253  xpdifid  5264  cnvcnvsn  5312  opswap  5322  mptpreima  5327  rnco  5340  ressn  5371  xpco  5375  wfi  5412  fncnv  5645  fununi  5647  fnres  5690  mptfnf  5697  fnopabg  5699  dff1o2  5817  eqfnfv3  5976  respreima  6007  fsn  6059  f13dfv  6171  fliftcnv  6202  isoini  6227  elrnmpt2res  6407  ndmovcom  6453  uniuni  6597  brtpos2  6976  brtpos  6979  tpostpos  6990  tposmpt2  7007  mpt2curryd  7013  oaord  7245  oeeu  7301  nnaord  7317  pmex  7474  elpmg  7484  mapval2  7498  mapsnen  7644  map1  7645  xpsnen  7653  xpcomco  7659  elfi2  7925  supmo  7963  infmo  8008  cp  8359  dfac5lem1  8551  dfac5lem2  8552  dfac5lem3  8553  dfac2  8558  kmlem3  8579  cdacomen  8608  cf0  8678  cflim3  8689  brdom7disj  8956  brdom6disj  8957  recmulnq  9386  letri3  9716  lesub0  10128  wloglei  10143  mulsuble0b  10474  creur  10600  indstr  11224  xrltlen  11442  xrletri3  11448  qbtwnre  11489  xmulcom  11549  xmulneg1  11552  xmulf  11555  iooneg  11749  iccneg  11750  elfzuzb  11791  fzrev  11855  ssfzoulel  12002  injresinj  12022  xpcogend  13031  rediv  13187  imdiv  13194  lenegsq  13376  o1lo1  13594  fsumcom2  13828  fsumcom  13829  fprodcom2  14031  fprodcom  14032  divalglem10  14376  smueqlem  14457  gcdcom  14477  lcmcom  14550  isprm2  14625  infpn2  14850  imasleval  15440  invsym  15660  dfiso3  15671  subsubc  15751  isffth2  15814  odulatb  16382  oduclatb  16383  posglbmo  16386  resscntz  16978  oppgid  17000  gsumcom  17602  dfrhm2  17938  lsslss  18177  fiidomfld  18525  opsrtoslem1  18700  xrsdsreclb  19008  znleval  19118  gsumcom3  19417  madutpos  19660  fvmptnn04if  19866  ntreq0  20086  restopn2  20186  ist0-3  20354  1stcelcls  20469  txkgen  20660  trfil2  20895  elflim2  20972  flimrest  20991  txflf  21014  fclsrest  21032  tsmssubm  21150  ismet2  21341  blres  21439  metrest  21532  restmetu  21578  xrtgioo  21817  elii1  21956  evthicc2  22404  ovolfcl  22412  ovoliunlem1  22448  dyaddisj  22547  mbfaddlem  22609  itg1climres  22665  mbfi1fseqlem4  22669  iblpos  22743  itgposval  22746  ditgsplit  22809  ellimc3  22827  itgsubst  22994  deg1ldg  23034  sincosq1sgn  23446  sincosq3sgn  23448  cos11  23475  dvdsflsumcom  24110  fsumvma  24134  logfaclbnd  24143  dchrelbas3  24159  lgsdi  24253  lgsquadlem1  24275  lgsquadlem2  24276  lgsquadlem3  24277  istrkg2ld  24501  tgcgr4  24569  mirreu3  24692  hpgcom  24802  colhp  24805  dfcgra2  24864  cusgra3v  25185  trls  25259  trlon  25263  pthon  25298  spthon  25305  3v3e3cycl2  25385  wwlkextinj  25451  clwwlkn2  25496  usg2spthonot0  25610  rusgranumwlkl1  25668  rusgra0edg  25676  eupath2lem2  25699  frg2wot1  25778  frg2woteqm  25780  usg2spot2nb  25786  usgreg2spot  25788  frgrareg  25838  frgraregord013  25839  h2hcau  26625  h2hlm  26626  axhcompl-zf  26644  nmopub  27554  nmfnleub  27571  chrelati  28010  cvexchlem  28014  mdsymlem8  28056  sumdmdii  28061  spc2ed  28099  reuxfr3d  28118  rmo3f  28124  rmo4fOLD  28125  2ndpreima  28281  fpwrelmapffslem  28310  xrofsup  28346  pmtrprfv2  28604  smatrcl  28615  cnvordtrestixx  28712  issgon  28938  eulerpartlemr  29200  eulerpartlemgvv  29202  ballotlem2  29314  sgn3da  29405  bnj257  29505  bnj545  29699  bnj594  29716  coep  30384  dfpo2  30388  dfdm5  30411  dfrn5  30412  elima4  30414  frind  30474  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-dfmpt2a  31623  bj-eldiag  31639  bj-ccinftydisj  31648  mptsnunlem  31733  topdifinffinlem  31743  wl-cases2-dnf  31843  wl-ax11-lem4  31911  fin2solem  31924  poimirlem4  31937  poimirlem26  31959  poimirlem30  31963  poimirlem32  31965  ftc1anclem6  32015  ftc1anc  32018  heibor1  32135  isdrngo3  32191  isdmn3  32300  prtlem70  32419  prtlem90  32425  lrelat  32574  islshpat  32577  atlrelat1  32881  ishlat2  32913  pmapglb  33329  polval2N  33465  cdlemb3  34167  diblsmopel  34733  dicelval3  34742  diclspsn  34756  fz1eqin  35605  diophrex  35612  fphpd  35653  fzneg  35826  expdioph  35872  dford4  35878  lnr2i  35969  fgraphopab  36081  ifpancor  36101  ifpdfbi  36111  ifpidg  36129  ifpid2g  36131  ifpid1g  36132  ifpim23g  36133  ifp1bi  36140  rp-fakeoranass  36152  dfid7  36213  dfrtrcl5  36230  relexp0eq  36287  isprm7  36654  uunT1p1  37162  uun132p1  37167  un2122  37171  uun2131p1  37173  uunT12p1  37181  uunT12p2  37182  uunT12p3  37183  uun2221  37194  uun2221p1  37195  uun2221p2  37196  3impdirp1  37197  ancomstVD  37256  mapsnend  37474  icccncfext  37759  dvnmul  37812  dvmptfprodlem  37813  dvnprodlem2  37816  fourierdlem42  38006  fourierdlem42OLD  38007  fourierdlem83  38047  2reu3  38603  2reu7  38606  2reu8  38607  ndmaovcom  38701  nbgrel  39393  nbgrsym  39420  usgra2pth0  39656  2zrngnmrid  39937  opeliun2xp  40101  eliunxp2  40102