MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancom Structured version   Visualization version   GIF version

Theorem ancom 465
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 ((𝜑𝜓) ↔ (𝜓𝜑))

Proof of Theorem ancom
StepHypRef Expression
1 pm3.22 464 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm3.22 464 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 198 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  ancomd  466  ancomst  467  ancomsd  469  pm4.71r  661  pm5.32ri  668  pm5.32rd  670  anbi2ci  728  anbi12ci  730  an12  834  an32  835  an13  836  an42  862  andir  908  dfbi3  933  dfifp6  1012  3anrot  1036  3ancoma  1038  nancom  1442  excxor  1461  cador  1538  cadcoma  1542  exancom  1774  19.42v  1905  19.42  2092  sbel2x  2447  moanmo  2520  2eu3  2543  2eu7  2547  2eu8  2548  eq2tri  2671  r19.28v  3053  r19.29r  3055  r19.42v  3073  rexcomf  3078  rabswap  3098  euxfr2  3358  rmo4  3366  reu8  3369  rmo3  3494  incom  3767  difin2  3849  euelss  3873  ssunsn  4300  inuni  4753  reuxfr2d  4817  eqvinop  4881  dfid3  4954  elxp2  5056  elvvv  5101  brinxp2  5103  dmuni  5256  dfres2  5372  restidsing  5377  dfima2  5387  imadmrn  5395  imai  5397  asymref2  5432  cnvxp  5470  xpdifid  5481  cnvcnvsn  5530  opswap  5540  mptpreima  5545  rnco  5558  ressn  5588  xpco  5592  wfi  5630  elon2  5651  fncnv  5876  fununi  5878  fnres  5921  mptfnf  5928  fnopabg  5930  dff1o2  6055  eqfnfv3  6221  respreima  6252  fsn  6308  f13dfv  6430  fliftcnv  6461  isoini  6488  elrnmpt2res  6672  ndmovcom  6719  uniuni  6865  brtpos2  7245  brtpos  7248  tpostpos  7259  tposmpt2  7276  mpt2curryd  7282  oaord  7514  oeeu  7570  nnaord  7586  pmex  7749  elpmg  7759  mapval2  7773  mapsnen  7920  map1  7921  xpsnen  7929  xpcomco  7935  elfi2  8203  supmo  8241  infmo  8284  cp  8637  dfac5lem1  8829  dfac5lem2  8830  dfac5lem3  8831  dfac2  8836  kmlem3  8857  cdacomen  8886  cf0  8956  cflim3  8967  brdom7disj  9234  brdom6disj  9235  recmulnq  9665  letri3  10002  lesub0  10424  wloglei  10439  mulsuble0b  10774  creur  10891  indstr  11632  xrltlen  11855  xrletri3  11861  qbtwnre  11904  xmulcom  11968  xmulneg1  11971  xmulf  11974  iooneg  12163  iccneg  12164  elfzuzb  12207  fzrev  12273  ssfzoulel  12428  injresinj  12451  xpcogend  13561  rediv  13719  imdiv  13726  lenegsq  13908  o1lo1  14116  fsumcom2  14347  fsumcom2OLD  14348  fsumcom  14349  fprodcom2  14553  fprodcom2OLD  14554  fprodcom  14555  divalglem10  14963  smueqlem  15050  gcdcom  15073  dfgcd2  15101  lcmcom  15144  isprm2  15233  isprm7  15258  infpn2  15455  imasleval  16024  invsym  16245  dfiso3  16256  subsubc  16336  isffth2  16399  odulatb  16966  oduclatb  16967  posglbmo  16970  resscntz  17587  oppgid  17609  gsumcom  18199  dfrhm2  18540  lsslss  18782  fiidomfld  19129  opsrtoslem1  19305  xrsdsreclb  19612  znleval  19722  gsumcom3  20024  madutpos  20267  fvmptnn04if  20473  ntreq0  20691  restopn2  20791  ist0-3  20959  1stcelcls  21074  txkgen  21265  trfil2  21501  elflim2  21578  flimrest  21597  txflf  21620  fclsrest  21638  tsmssubm  21756  ismet2  21948  blres  22046  metrest  22139  restmetu  22185  xrtgioo  22417  elii1  22542  isclmp  22705  isncvsngp  22757  evthicc2  23036  ovolfcl  23042  ovoliunlem1  23077  dyaddisj  23170  mbfaddlem  23233  itg1climres  23287  mbfi1fseqlem4  23291  iblpos  23365  itgposval  23368  ditgsplit  23431  ellimc3  23449  itgsubst  23616  deg1ldg  23656  sincosq1sgn  24054  sincosq3sgn  24056  cos11  24083  dvdsflsumcom  24714  fsumvma  24738  logfaclbnd  24747  dchrelbas3  24763  lgsdi  24859  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  2lgslem1a  24916  istrkg2ld  25159  tgcgr4  25226  mirreu3  25349  hpgcom  25459  colhp  25462  dfcgra2  25521  cusgra3v  25993  trls  26066  trlon  26070  pthon  26105  spthon  26112  3v3e3cycl2  26192  wwlkextinj  26258  clwwlkn2  26303  usg2spthonot0  26416  rusgranumwlkl1  26474  rusgra0edg  26482  eupath2lem2  26505  frg2wot1  26584  frg2woteqm  26586  usg2spot2nb  26592  usgreg2spot  26594  frgrareg  26644  frgraregord013  26645  h2hcau  27220  h2hlm  27221  axhcompl-zf  27239  nmopub  28151  nmfnleub  28168  chrelati  28607  cvexchlem  28611  mdsymlem8  28653  sumdmdii  28658  spc2ed  28696  reuxfr3d  28713  rmo3f  28719  rmo4fOLD  28720  2ndpreima  28868  fpwrelmapffslem  28895  xrofsup  28923  pmtrprfv2  29179  smatrcl  29190  cnvordtrestixx  29287  issgon  29513  eulerpartlemr  29763  eulerpartlemgvv  29765  ballotlem2  29877  sgn3da  29930  bnj257  30026  bnj545  30219  bnj594  30236  coep  30894  dfpo2  30898  dfdm5  30921  dfrn5  30922  elima4  30924  frind  30984  nocvxmin  31090  brtxp  31157  elfix  31180  dffix2  31182  sscoid  31190  brimg  31214  brsuccf  31218  funpartfun  31220  dfrecs2  31227  dfrdg4  31228  cgrcomlr  31275  ofscom  31284  btwnexch  31302  fscgr  31357  bj-dfifc2  31734  bj-restuni  32231  bj-dfmpt2a  32252  bj-eldiag  32268  bj-ccinftydisj  32277  mptsnunlem  32361  topdifinffinlem  32371  wl-cases2-dnf  32474  wl-ax11-lem4  32544  fin2solem  32565  poimirlem4  32583  poimirlem26  32605  poimirlem30  32609  poimirlem32  32611  ftc1anclem6  32660  ftc1anc  32663  heibor1  32779  isdrngo3  32928  isdmn3  33043  prtlem70  33157  lrelat  33319  islshpat  33322  atlrelat1  33626  ishlat2  33658  pmapglb  34074  polval2N  34210  cdlemb3  34912  diblsmopel  35478  dicelval3  35487  diclspsn  35501  fz1eqin  36350  diophrex  36357  fphpd  36398  fzneg  36567  expdioph  36608  dford4  36614  lnr2i  36705  fgraphopab  36807  ifpancor  36827  ifpdfbi  36837  ifpidg  36855  ifpid2g  36857  ifpid1g  36858  ifpim23g  36859  ifp1bi  36866  rp-fakeoranass  36878  dfid7  36938  dfrtrcl5  36955  relexp0eq  37012  fsovrfovd  37323  rcompleq  37338  uunT1p1  38029  uun132p1  38034  un2122  38038  uun2131p1  38040  uunT12p1  38048  uunT12p2  38049  uunT12p3  38050  uun2221  38061  uun2221p1  38062  uun2221p2  38063  3impdirp1  38064  ancomstVD  38123  mapsnend  38386  icccncfext  38773  dvnmul  38833  dvmptfprodlem  38834  dvnprodlem2  38837  fourierdlem42  39042  fourierdlem83  39082  2reu3  39837  2reu7  39840  2reu8  39841  ndmaovcom  39934  mptmpt2opabbrd  40335  nbgrel  40564  nbgrsym  40591  wlkson  40864  isspthonpth-av  40955  usgr2pth0  40971  wwlksnextinj  41105  elwspths2spth  41171  rusgrnumwwlkl1  41172  clwwlksn2  41217  iseupthf1o  41369  eupth2lem2  41387  frgr2wwlk1  41494  fusgreg2wsp  41500  av-numclwwlkovf2  41515  av-frgrareg  41548  av-frgraregord013  41549  2zrngnmrid  41740  opeliun2xp  41904  eliunxp2  41905
  Copyright terms: Public domain W3C validator