Theorem ancom 457

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

Syntax hints:   <-> wb 189   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  ancomd  458  ancomst  459  ancomsd  461  pm4.71r  643  pm5.32ri  650  pm5.32rd  652  anbi2ci  710  anbi12ci  712  an12  814  an32  815  an13  816  an42  841  andir  885  dfbi3  910  dfifp6  989  3anrot  1012  3ancoma  1014  nancom  1415  excxor  1436  cador  1519  cadcoma  1523  exancom  1730  19.42v  1842  19.42  2071  sbel2x  2308  moanmo  2381  2eu3  2404  2eu7  2408  2eu8  2409  eq2tri  2532  r19.28v  2911  r19.29r  2913  r19.42v  2931  rexcomf  2936  rabswap  2956  euxfr2  3211  rmo4  3219  reu8  3222  rmo3  3344  incom  3616  difin2  3696  euelss  3721  difin0ss  3745  ssunsn  4124  inuni  4563  reuxfr2d  4623  eqvinop  4686  dfid3  4755  elvvv  4899  brinxp2  4901  dmuni  5050  dfres2  5163  dfima2  5176  imadmrn  5184  imai  5186  asymref2  5223  cnvxp  5260  xpdifid  5271  cnvcnvsn  5320  opswap  5330  mptpreima  5335  rnco  5348  ressn  5379  xpco  5383  wfi  5420  fncnv  5657  fununi  5659  fnres  5702  mptfnf  5709  fnopabg  5711  dff1o2  5833  eqfnfv3  5993  respreima  6024  fsn  6077  f13dfv  6191  fliftcnv  6222  isoini  6247  elrnmpt2res  6429  ndmovcom  6475  uniuni  6619  brtpos2  6997  brtpos  7000  tpostpos  7011  tposmpt2  7028  mpt2curryd  7034  oaord  7266  oeeu  7322  nnaord  7338  pmex  7495  elpmg  7505  mapval2  7519  mapsnen  7665  map1  7666  xpsnen  7674  xpcomco  7680  elfi2  7946  supmo  7984  infmo  8029  cp  8380  dfac5lem1  8572  dfac5lem2  8573  dfac5lem3  8574  dfac2  8579  kmlem3  8600  cdacomen  8629  cf0  8699  cflim3  8710  brdom7disj  8977  brdom6disj  8978  recmulnq  9407  letri3  9737  lesub0  10152  wloglei  10167  mulsuble0b  10499  creur  10625  indstr  11250  xrltlen  11468  xrletri3  11474  qbtwnre  11515  xmulcom  11577  xmulneg1  11580  xmulf  11583  iooneg  11778  iccneg  11779  elfzuzb  11820  fzrev  11884  ssfzoulel  12034  injresinj  12057  xpcogend  13113  rediv  13271  imdiv  13278  lenegsq  13460  o1lo1  13678  fsumcom2  13912  fsumcom  13913  fprodcom2  14115  fprodcom  14116  divalglem10  14462  smueqlem  14543  gcdcom  14563  lcmcom  14636  isprm2  14711  infpn2  14936  imasleval  15525  invsym  15745  dfiso3  15756  subsubc  15836  isffth2  15899  odulatb  16467  oduclatb  16468  posglbmo  16471  resscntz  17063  oppgid  17085  gsumcom  17687  dfrhm2  18023  lsslss  18262  fiidomfld  18609  opsrtoslem1  18784  xrsdsreclb  19092  znleval  19202  gsumcom3  19501  madutpos  19744  fvmptnn04if  19950  ntreq0  20170  restopn2  20270  ist0-3  20438  1stcelcls  20553  txkgen  20744  trfil2  20980  elflim2  21057  flimrest  21076  txflf  21099  fclsrest  21117  tsmssubm  21235  ismet2  21426  blres  21524  metrest  21617  restmetu  21663  xrtgioo  21902  elii1  22041  evthicc2  22489  ovolfcl  22497  ovoliunlem1  22533  dyaddisj  22633  mbfaddlem  22695  itg1climres  22751  mbfi1fseqlem4  22755  iblpos  22829  itgposval  22832  ditgsplit  22895  ellimc3  22913  itgsubst  23080  deg1ldg  23120  sincosq1sgn  23532  sincosq3sgn  23534  cos11  23561  dvdsflsumcom  24196  fsumvma  24220  logfaclbnd  24229  dchrelbas3  24245  lgsdi  24339  lgsquadlem1  24361  lgsquadlem2  24362  lgsquadlem3  24363  istrkg2ld  24587  tgcgr4  24655  mirreu3  24778  hpgcom  24888  colhp  24891  dfcgra2  24950  cusgra3v  25271  trls  25345  trlon  25349  pthon  25384  spthon  25391  3v3e3cycl2  25471  wwlkextinj  25537  clwwlkn2  25582  usg2spthonot0  25696  rusgranumwlkl1  25754  rusgra0edg  25762  eupath2lem2  25785  frg2wot1  25864  frg2woteqm  25866  usg2spot2nb  25872  usgreg2spot  25874  frgrareg  25924  frgraregord013  25925  h2hcau  26713  h2hlm  26714  axhcompl-zf  26732  nmopub  27642  nmfnleub  27659  chrelati  28098  cvexchlem  28102  mdsymlem8  28144  sumdmdii  28149  spc2ed  28187  reuxfr3d  28204  rmo3f  28210  rmo4fOLD  28211  2ndpreima  28363  fpwrelmapffslem  28392  xrofsup  28428  pmtrprfv2  28685  smatrcl  28696  cnvordtrestixx  28793  issgon  29019  eulerpartlemr  29280  eulerpartlemgvv  29282  ballotlem2  29394  sgn3da  29485  bnj257  29584  bnj545  29778  bnj594  29795  coep  30462  dfpo2  30466  dfdm5  30489  dfrn5  30490  elima4  30492  frind  30552  nocvxmin  30651  brtxp  30718  elfix  30741  dffix2  30743  sscoid  30751  brimg  30775  brsuccf  30779  funpartfun  30781  dfrecs2  30788  dfrdg4  30789  cgrcomlr  30836  ofscom  30845  btwnexch  30863  fscgr  30918  bj-dfifc2  31222  bj-dfmpt2a  31700  bj-eldiag  31716  bj-ccinftydisj  31725  mptsnunlem  31810  topdifinffinlem  31820  wl-cases2-dnf  31920  wl-ax11-lem4  31982  fin2solem  31995  poimirlem4  32008  poimirlem26  32030  poimirlem30  32034  poimirlem32  32036  ftc1anclem6  32086  ftc1anc  32089  heibor1  32206  isdrngo3  32262  isdmn3  32371  prtlem70  32489  prtlem90  32495  lrelat  32651  islshpat  32654  atlrelat1  32958  ishlat2  32990  pmapglb  33406  polval2N  33542  cdlemb3  34244  diblsmopel  34810  dicelval3  34819  diclspsn  34833  fz1eqin  35682  diophrex  35689  fphpd  35730  fzneg  35903  expdioph  35949  dford4  35955  lnr2i  36046  fgraphopab  36158  ifpancor  36178  ifpdfbi  36188  ifpidg  36206  ifpid2g  36208  ifpid1g  36209  ifpim23g  36210  ifp1bi  36217  rp-fakeoranass  36229  dfid7  36290  dfrtrcl5  36307  relexp0eq  36364  isprm7  36730  uunT1p1  37231  uun132p1  37236  un2122  37240  uun2131p1  37242  uunT12p1  37250  uunT12p2  37251  uunT12p3  37252  uun2221  37263  uun2221p1  37264  uun2221p2  37265  3impdirp1  37266  ancomstVD  37325  mapsnend  37551  icccncfext  37862  dvnmul  37915  dvmptfprodlem  37916  dvnprodlem2  37919  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem83  38165  2reu3  38754  2reu7  38757  2reu8  38758  ndmaovcom  38852  mptmpt2opabbrd  39180  nbgrel  39574  nbgrsym  39601  wlkson  39854  isspthonpth-av  39941  iseupthf1o  40114  eupth2lem2  40131  usgra2pth0  40177  2zrngnmrid  40458  opeliun2xp  40622  eliunxp2  40623