Theorem ancom 450

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

Syntax hints:   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  ancomd  451  ancomst  452  ancomsd  454  pm4.71r  631  pm5.32ri  638  pm5.32rd  640  anbi2ci  696  anbi12ci  698  an12  797  an32  798  an13  799  an42  825  andir  868  dfbi3  893  rbaibOLD  907  rbaibrOLD  908  3anrot  978  3ancoma  980  nancom  1346  nancomOLD  1347  excxor  1368  dfifp6  1386  cador  1458  cadcoma  1462  cadcomb  1463  cad1  1465  exancom  1672  19.42v  1776  19.42  1973  sbel2x  2204  moanmo  2353  2eu3  2379  2eu6OLD  2384  2eu7  2385  2eu8  2386  eq2tri  2525  r19.28v  2991  r19.29r  2993  r19.42v  3012  rexcomf  3017  rabswap  3037  euxfr2  3284  rmo4  3292  reu8  3295  rmo3  3425  incom  3687  difin2  3767  euelss  3792  difin0ss  3897  ssunsn  4192  inuni  4618  reuxfr2d  4679  eqvinop  4740  dfid3  4805  elvvv  5068  brinxp2  5070  dmuni  5222  dfres2  5336  dfima2  5349  imadmrn  5357  imai  5359  asymref2  5394  cnvxp  5431  xpdifid  5442  cnvcnvsn  5491  opswap  5501  mptpreima  5506  rnco  5519  ressn  5549  xpco  5553  fncnv  5658  fununi  5660  fnres  5703  fnopabg  5710  dff1o2  5827  eqfnfv3  5984  respreima  6017  fsn  6070  f13dfv  6181  fliftcnv  6210  isoini  6235  elrnmpt2res  6415  ndmovcom  6461  uniuni  6608  brtpos2  6979  brtpos  6982  tpostpos  6993  tposmpt2  7010  mpt2curryd  7016  oaord  7214  oeeu  7270  nnaord  7286  pmex  7443  elpmg  7453  mapval2  7467  mapsnen  7612  map1  7613  xpsnen  7620  xpcomco  7626  elfi2  7892  supmo  7929  cp  8326  dfac5lem1  8521  dfac5lem2  8522  dfac5lem3  8523  dfac2  8528  kmlem3  8549  cdacomen  8578  cf0  8648  cflim3  8659  brdom7disj  8926  brdom6disj  8927  recmulnq  9359  letri3  9687  lesub0  10090  wloglei  10106  mulsuble0b  10435  creur  10550  indstr  11175  xrltlen  11377  xrletri3  11383  qbtwnre  11423  xmulcom  11483  xmulneg1  11486  xmulf  11489  iooneg  11665  iccneg  11666  elfzuzb  11707  fzrev  11767  ssfzoulel  11908  injresinj  11928  rediv  12975  imdiv  12982  lenegsq  13164  o1lo1  13371  fsumcom2  13600  fsumcom  13601  fprodcom2  13799  fprodcom  13800  divalglem10  14071  smueqlem  14151  gcdcom  14169  isprm2  14236  infpn2  14442  imasleval  14957  invsym  15177  dfiso3  15188  subsubc  15268  isffth2  15331  odulatb  15899  oduclatb  15900  posglbmo  15903  resscntz  16495  oppgid  16517  gsumcom  17131  dfrhm2  17492  lsslss  17733  fiidomfld  18083  opsrtoslem1  18274  xrsdsreclb  18591  znleval  18719  gsumcom3  19027  madutpos  19270  fvmptnn04if  19476  istps3OLD  19549  ntreq0  19704  restopn2  19804  ist0-3  19972  1stcelcls  20087  txkgen  20278  trfil2  20513  elflim2  20590  flimrest  20609  txflf  20632  fclsrest  20650  tsmssubm  20769  ismet2  20961  blres  21059  metrest  21152  restmetu  21215  xrtgioo  21436  elii1  21560  evthicc2  21997  ovolfcl  22003  ovoliunlem1  22038  dyaddisj  22130  mbfaddlem  22192  itg1climres  22246  mbfi1fseqlem4  22250  iblpos  22324  itgposval  22327  ditgsplit  22390  ellimc3  22408  itgsubst  22575  deg1ldg  22617  sincosq1sgn  23016  sincosq3sgn  23018  cos11  23045  dvdsflsumcom  23589  fsumvma  23613  logfaclbnd  23622  dchrelbas3  23638  lgsdi  23732  lgsquadlem1  23754  lgsquadlem2  23755  lgsquadlem3  23756  istrkg2ld  23983  mirreu3  24160  hpgcom  24261  cusgra3v  24590  trls  24664  trlon  24668  pthon  24703  spthon  24710  3v3e3cycl2  24790  wwlkextinj  24856  clwwlkn2  24901  usg2spthonot0  25015  rusgranumwlkl1  25073  rusgra0edg  25081  eupath2lem2  25104  frg2wot1  25183  frg2woteqm  25185  usg2spot2nb  25191  usgreg2spot  25193  frgrareg  25243  frgraregord013  25244  h2hcau  26022  h2hlm  26023  axhcompl-zf  26041  nmopub  26953  nmfnleub  26970  chrelati  27409  cvexchlem  27413  mdsymlem8  27455  sumdmdii  27460  spc2ed  27498  reuxfr3d  27514  rmo3f  27520  rmo4fOLD  27521  mptfnf  27642  2ndpreima  27674  fpwrelmapffslem  27705  xrofsup  27734  cnvordtrestixx  28048  issgon  28284  eulerpartlemr  28488  eulerpartlemgvv  28490  ballotlem2  28602  sgn3da  28655  coep  29355  dfpo2  29359  dfdm5  29380  dfrn5  29381  elima4  29383  wfi  29461  frind  29497  nocvxmin  29625  brtxp  29692  elfix  29715  dffix2  29717  sscoid  29725  brimg  29749  funpartfun  29755  dfrdg4  29762  tfrqfree  29763  cgrcomlr  29810  ofscom  29819  btwnexch  29837  fscgr  29892  wl-ax11-lem4  30190  fin2solem  30201  ftc1anclem6  30257  ftc1anc  30260  heibor1  30468  isdrngo3  30524  isdmn3  30633  an43OLD  30752  prtlem70  30754  prtlem90  30760  fz1eqin  30864  diophrex  30871  fphpd  30912  fzneg  31082  expdioph  31127  dford4  31133  lnr2i  31227  fgraphopab  31332  isprm7  31354  lcmcom  31361  icccncfext  31851  dvnmul  31901  dvmptfprodlem  31902  dvnprodlem2  31905  fourierdlem42  32092  fourierdlem83  32133  2reu3  32354  2reu7  32357  2reu8  32358  ndmaovcom  32451  usgra2pth0  32575  2zrngnmrid  32858  opeliun2xp  33024  eliunxp2  33025  uunT1p1  33679  uun132p1  33684  un2122  33688  uun2131p1  33690  uunT12p1  33698  uunT12p2  33699  uunT12p3  33700  uun2221  33711  uun2221p1  33712  uun2221p2  33713  3impdirp1  33714  ancomstVD  33766  bnj257  33860  bnj545  34054  bnj594  34071  bj-dfifc2  34265  bj-eldiag  34707  bj-ccinftydisj  34717  lrelat  34840  islshpat  34843  atlrelat1  35147  ishlat2  35179  pmapglb  35595  polval2N  35731  cdlemb3  36433  diblsmopel  36999  dicelval3  37008  diclspsn  37022  bj-ifidg  37808  bj-ifid1g  37809  bj-ifid2g  37810  bj-if1bi  37821  bj-ifdfbi  37831  rp-fakeoranass  37839  xpcogend  37874