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  795  an32  796  an13  797  an42  823  andir  866  dfbi3  891  rbaibOLD  905  rbaibrOLD  906  jaoi2OLD  967  3anrot  978  3ancoma  980  nancom  1346  excxor  1365  cador  1442  cadcoma  1447  cadcomb  1448  cad1  1450  exancom  1648  19.42  1921  sbel2x  2191  eu1OLD  2326  moanmo  2357  moaneuOLD  2359  2eu3  2389  2eu6OLD  2394  2eu7  2395  2eu8  2396  eq2tri  2535  r19.28av  3001  r19.29r  3003  r19.42v  3021  rexcomf  3026  rabswap  3046  euxfr2  3293  rmo4  3301  reu8  3304  rmo3  3435  incom  3696  difin2  3765  difin0ss  3899  ssunsn  4193  inuni  4615  reuxfr2d  4676  eqvinop  4737  dfid3  4802  elvvv  5065  brinxp2  5067  dmuni  5218  dfres2  5332  dfima2  5345  imadmrn  5353  imai  5355  asymref2  5390  cnvxp  5430  xpdifid  5441  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  6179  fliftcnv  6208  isoini  6233  elrnmpt2res  6411  ndmovcom  6457  uniuni  6604  brtpos2  6973  brtpos  6976  tpostpos  6987  tposmpt2  7004  mpt2curryd  7010  oaord  7208  oeeu  7264  nnaord  7280  pmex  7437  elpmg  7446  mapval2  7460  mapsnen  7605  map1  7606  xpsnen  7613  xpcomco  7619  elfi2  7886  supmo  7924  cp  8321  dfac5lem1  8516  dfac5lem2  8517  dfac5lem3  8518  dfac2  8523  kmlem3  8544  cdacomen  8573  cf0  8643  cflim3  8654  brdom7disj  8921  brdom6disj  8922  recmulnq  9354  letri3  9682  lesub0  10081  wloglei  10097  mulsuble0b  10426  creur  10542  indstr  11162  xrltlen  11364  xrletri3  11370  qbtwnre  11410  xmulcom  11470  xmulneg1  11473  xmulf  11476  iooneg  11652  iccneg  11653  elfzuzb  11694  fzrev  11754  fzm1  11770  ssfzoulel  11886  injresinj  11906  wrdeqswrdlsw  12653  rediv  12943  imdiv  12950  lenegsq  13132  o1lo1  13339  fsumcom2  13568  fsumcom  13569  divalglem10  13935  smueqlem  14015  gcdcom  14033  isprm2  14100  infpn2  14306  imasleval  14812  invsym  15033  subsubc  15096  isffth2  15159  odulatb  15646  oduclatb  15647  posglbmo  15650  resscntz  16240  oppgid  16262  gsumcom  16876  dfrhm2  17236  lsslss  17476  fiidomfld  17825  opsrtoslem1  18016  xrsdsreclb  18333  znleval  18460  gsumcom3  18768  madutpos  19011  fvmptnn04if  19217  istps3OLD  19290  ntreq0  19444  restopn2  19544  ist0-3  19712  1stcelcls  19828  txkgen  20019  trfil2  20254  elflim2  20331  flimrest  20350  txflf  20373  fclsrest  20391  tsmssubm  20510  ismet2  20702  blres  20800  metrest  20893  restmetu  20956  xrtgioo  21177  elii1  21301  evthicc2  21738  ovolfcl  21744  ovoliunlem1  21779  dyaddisj  21871  mbfaddlem  21933  itg1climres  21987  mbfi1fseqlem4  21991  iblpos  22065  itgposval  22068  ditgsplit  22131  ellimc3  22149  itgsubst  22316  deg1ldg  22358  sincosq1sgn  22755  sincosq3sgn  22757  cos11  22784  dvdsflsumcom  23328  fsumvma  23352  logfaclbnd  23361  dchrelbas3  23377  lgsdi  23471  lgsquadlem1  23493  lgsquadlem2  23494  lgsquadlem3  23495  istrkg2ld  23722  mirreu3  23893  cusgra3v  24296  trls  24370  trlon  24374  pthon  24409  spthon  24416  3v3e3cycl2  24496  clwwlkn2  24607  usg2spthonot0  24721  rusgranumwlkl1  24779  rusgra0edg  24787  eupath2lem2  24810  frg2wot1  24889  frg2woteqm  24891  usg2spot2nb  24897  usgreg2spot  24899  frgrareg  24949  frgraregord013  24950  h2hcau  25727  h2hlm  25728  axhcompl-zf  25746  nmopub  26658  nmfnleub  26675  chrelati  27114  cvexchlem  27118  mdsymlem8  27160  sumdmdii  27165  spc2ed  27203  reuxfr3d  27219  rmo3f  27225  rmo4fOLD  27226  mptfnf  27330  2ndpreima  27356  fpwrelmapffslem  27386  xrofsup  27413  cnvordtrestixx  27727  issgon  27955  eulerpartlemr  28145  eulerpartlemgvv  28147  ballotlem2  28259  sgn3da  28312  fprodcom2  29048  fprodcom  29049  coep  29114  dfpo2  29118  dfdm5  29140  dfrn5  29141  elima4  29143  wfi  29221  frind  29257  nocvxmin  29385  brtxp  29464  elfix  29487  dffix2  29489  sscoid  29497  brimg  29521  funpartfun  29527  dfrdg4  29534  tfrqfree  29535  cgrcomlr  29582  ofscom  29591  btwnexch  29609  fscgr  29664  wl-ax11-lem4  29962  fin2solem  29973  ftc1anclem6  30029  ftc1anc  30032  heibor1  30240  isdrngo3  30296  isdmn3  30405  an43OLD  30524  prtlem70  30526  prtlem90  30532  fz1eqin  30636  diophrex  30643  fphpd  30684  fzneg  30854  expdioph  30899  dford4  30905  lnr2i  30999  fgraphopab  31105  isprm7  31125  lcmcom  31129  icccncfext  31555  fourierdlem42  31778  fourierdlem83  31819  2reu3  31989  2reu7  31992  2reu8  31993  ndmaovcom  32086  usgra2pth0  32151  2zrngnmrid  32356  opeliun2xp  32407  eliunxp2  32408  uunT1p1  33064  uun132p1  33069  un2122  33073  uun2131p1  33075  uunT12p1  33083  uunT12p2  33084  uunT12p3  33085  uun2221  33096  uun2221p1  33097  uun2221p2  33098  3impdirp1  33099  ancomstVD  33151  bnj257  33245  bnj545  33438  bnj594  33455  bj-dfif6  33637  bj-dfifc2  33651  bj-eldiag  34084  bj-ccinftydisj  34094  lrelat  34217  islshpat  34220  atlrelat1  34524  ishlat2  34556  pmapglb  34972  polval2N  35108  cdlemb3  35808  diblsmopel  36374  dicelval3  36383  diclspsn  36397  xpcogend  37192