Theorem ancom 448

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

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

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 369

This theorem is referenced by:  ancomd  449  ancomst  450  ancomsd  452  pm4.71r  629  pm5.32ri  636  pm5.32rd  638  anbi2ci  694  anbi12ci  696  an12  798  an32  799  an13  800  an42  826  andir  869  dfbi3  894  rbaibOLD  908  rbaibrOLD  909  3anrot  979  3ancoma  981  nancom  1348  nancomOLD  1349  excxor  1372  dfifp6  1392  cador  1472  cadorOLD  1473  cadcoma  1479  cadcombOLD  1481  cad1OLD  1484  exancom  1692  19.42v  1799  19.42  2000  sbel2x  2227  moanmo  2304  2eu3  2330  2eu6OLD  2335  2eu7  2336  2eu8  2337  eq2tri  2470  r19.28v  2941  r19.29r  2943  r19.42v  2962  rexcomf  2967  rabswap  2987  euxfr2  3234  rmo4  3242  reu8  3245  rmo3  3368  incom  3632  difin2  3712  euelss  3737  difin0ss  3838  ssunsn  4132  inuni  4556  reuxfr2d  4614  eqvinop  4675  dfid3  4739  elvvv  4883  brinxp2  4885  dmuni  5033  dfres2  5146  dfima2  5159  imadmrn  5167  imai  5169  asymref2  5205  cnvxp  5242  xpdifid  5253  cnvcnvsn  5301  opswap  5311  mptpreima  5316  rnco  5329  ressn  5360  xpco  5364  wfi  5400  fncnv  5633  fununi  5635  fnres  5678  mptfnf  5685  fnopabg  5687  dff1o2  5804  eqfnfv3  5961  respreima  5994  fsn  6048  f13dfv  6161  fliftcnv  6192  isoini  6217  elrnmpt2res  6397  ndmovcom  6443  uniuni  6591  brtpos2  6964  brtpos  6967  tpostpos  6978  tposmpt2  6995  mpt2curryd  7001  oaord  7233  oeeu  7289  nnaord  7305  pmex  7462  elpmg  7472  mapval2  7486  mapsnen  7631  map1  7632  xpsnen  7639  xpcomco  7645  elfi2  7908  supmo  7945  cp  8341  dfac5lem1  8536  dfac5lem2  8537  dfac5lem3  8538  dfac2  8543  kmlem3  8564  cdacomen  8593  cf0  8663  cflim3  8674  brdom7disj  8941  brdom6disj  8942  recmulnq  9372  letri3  9701  lesub0  10110  wloglei  10125  mulsuble0b  10455  creur  10570  indstr  11195  xrltlen  11405  xrletri3  11411  qbtwnre  11451  xmulcom  11511  xmulneg1  11514  xmulf  11517  iooneg  11694  iccneg  11695  elfzuzb  11736  fzrev  11797  ssfzoulel  11943  injresinj  11963  xpcogend  12957  rediv  13113  imdiv  13120  lenegsq  13302  o1lo1  13509  fsumcom2  13740  fsumcom  13741  fprodcom2  13940  fprodcom  13941  divalglem10  14269  smueqlem  14349  gcdcom  14367  isprm2  14434  infpn2  14640  imasleval  15155  invsym  15375  dfiso3  15386  subsubc  15466  isffth2  15529  odulatb  16097  oduclatb  16098  posglbmo  16101  resscntz  16693  oppgid  16715  gsumcom  17326  dfrhm2  17686  lsslss  17927  fiidomfld  18277  opsrtoslem1  18468  xrsdsreclb  18785  znleval  18891  gsumcom3  19193  madutpos  19436  fvmptnn04if  19642  istps3OLD  19715  ntreq0  19871  restopn2  19971  ist0-3  20139  1stcelcls  20254  txkgen  20445  trfil2  20680  elflim2  20757  flimrest  20776  txflf  20799  fclsrest  20817  tsmssubm  20936  ismet2  21128  blres  21226  metrest  21319  restmetu  21382  xrtgioo  21603  elii1  21727  evthicc2  22164  ovolfcl  22170  ovoliunlem1  22205  dyaddisj  22297  mbfaddlem  22359  itg1climres  22413  mbfi1fseqlem4  22417  iblpos  22491  itgposval  22494  ditgsplit  22557  ellimc3  22575  itgsubst  22742  deg1ldg  22784  sincosq1sgn  23183  sincosq3sgn  23185  cos11  23212  dvdsflsumcom  23845  fsumvma  23869  logfaclbnd  23878  dchrelbas3  23894  lgsdi  23988  lgsquadlem1  24010  lgsquadlem2  24011  lgsquadlem3  24012  istrkg2ld  24236  mirreu3  24420  hpgcom  24524  colhp  24527  dfcgra2  24579  cusgra3v  24881  trls  24955  trlon  24959  pthon  24994  spthon  25001  3v3e3cycl2  25081  wwlkextinj  25147  clwwlkn2  25192  usg2spthonot0  25306  rusgranumwlkl1  25364  rusgra0edg  25372  eupath2lem2  25395  frg2wot1  25474  frg2woteqm  25476  usg2spot2nb  25482  usgreg2spot  25484  frgrareg  25534  frgraregord013  25535  h2hcau  26310  h2hlm  26311  axhcompl-zf  26329  nmopub  27240  nmfnleub  27257  chrelati  27696  cvexchlem  27700  mdsymlem8  27742  sumdmdii  27747  spc2ed  27785  reuxfr3d  27803  rmo3f  27809  rmo4fOLD  27810  2ndpreima  27970  fpwrelmapffslem  28002  xrofsup  28030  cnvordtrestixx  28348  issgon  28571  eulerpartlemr  28819  eulerpartlemgvv  28821  ballotlem2  28933  sgn3da  28986  bnj257  29086  bnj545  29280  bnj594  29297  coep  29964  dfpo2  29968  dfdm5  29991  dfrn5  29992  elima4  29994  frind  30054  nocvxmin  30151  brtxp  30218  elfix  30241  dffix2  30243  sscoid  30251  brimg  30275  brsuccf  30279  funpartfun  30281  dfrecs2  30288  dfrdg4  30289  cgrcomlr  30336  ofscom  30345  btwnexch  30363  fscgr  30418  bj-dfifc2  30728  bj-eldiag  31171  bj-ccinftydisj  31180  mptsnunlem  31254  topdifinffinlem  31264  wl-cases2-dnf  31337  wl-ax11-lem4  31400  fin2solem  31411  ftc1anclem6  31468  ftc1anc  31471  heibor1  31588  isdrngo3  31644  isdmn3  31753  an43OLD  31872  prtlem70  31874  prtlem90  31880  lrelat  32032  islshpat  32035  atlrelat1  32339  ishlat2  32371  pmapglb  32787  polval2N  32923  cdlemb3  33625  diblsmopel  34191  dicelval3  34200  diclspsn  34214  fz1eqin  35063  diophrex  35070  fphpd  35111  fzneg  35281  expdioph  35327  dford4  35333  lnr2i  35429  fgraphopab  35534  ifpancor  35554  ifpdfbi  35564  ifpidg  35582  ifpid2g  35584  ifpid1g  35585  ifpim23g  35586  ifp1bi  35593  rp-fakeoranass  35605  relexp0eq  35680  isprm7  36040  lcmcom  36047  uunT1p1  36602  uun132p1  36607  un2122  36611  uun2131p1  36613  uunT12p1  36621  uunT12p2  36622  uunT12p3  36623  uun2221  36634  uun2221p1  36635  uun2221p2  36636  3impdirp1  36637  ancomstVD  36696  icccncfext  37058  dvnmul  37108  dvmptfprodlem  37109  dvnprodlem2  37112  fourierdlem42  37299  fourierdlem83  37340  2reu3  37561  2reu7  37564  2reu8  37565  ndmaovcom  37658  usgra2pth0  37984  2zrngnmrid  38267  opeliun2xp  38433  eliunxp2  38434