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

Theorem com23 86
Description: Commutation of antecedents. Swap 2nd and 3rd. Deduction associated with com12 32. (Contributed by NM, 27-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com3.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
com23 (𝜑 → (𝜒 → (𝜓𝜃)))

Proof of Theorem com23
StepHypRef Expression
1 com3.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 pm2.27 42 . 2 (𝜒 → ((𝜒𝜃) → 𝜃))
31, 2syl9 77 1 (𝜑 → (𝜒 → (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com3r  87  com13  88  pm2.04  90  pm2.86d  108  impcomd  415  expcomd  420  impancom  455  a2and  842  dedlem0b  1040  sbequ1  2250  moexexlem  2712  ralrimdvva  3184  ceqsalt  3502  vtoclgft  3528  vtoclgftOLD  3529  sbciegft  3783  reupick  4261  reusv3  5283  sbcop1  5356  propeqop  5374  pwssun  5433  wefrc  5526  ssrel  5634  ssrel2  5636  ssrelrel  5646  ssrelrn  5740  predpo  6144  tz7.7  6195  ordtr2  6213  onmindif  6258  unizlim  6285  funssres  6377  f1ssf1  6628  fvmptt  6770  fveqdmss  6828  fvcofneq  6841  funsndifnop  6895  funfvima2  6976  isoini  7075  isopolem  7082  weniso  7091  f1ocnv2d  7383  limsssuc  7550  tfindsg  7560  limomss  7570  findsg  7595  funcnvuni  7622  f1oweALT  7659  funelss  7732  bropopvvv  7772  bropfvvvvlem  7773  bropfvvvv  7774  f1o2ndf1  7805  frxp  7807  suppfnss  7842  wfrlem12  7953  onfununi  7965  tz7.49  8068  omordi  8179  omlimcl  8191  omass  8193  oeordsuc  8207  nnmordi  8244  nnmord  8245  omabs  8261  xpdom2  8599  infensuc  8683  findcard2  8746  findcard2d  8748  findcard3  8749  frfi  8751  xpfi  8777  fsuppres  8846  dffi2  8875  elfiun  8882  ordiso2  8967  ordtypelem7  8976  suc11reg  9070  inf3lem2  9080  noinfep  9111  cantnfle  9122  cantnflem1  9140  cantnf  9144  trcl  9158  epfrs  9161  r1sdom  9191  updjud  9351  pr2ne  9420  dfac8alem  9444  indcardi  9456  alephordi  9489  dfac12lem3  9560  pwsdompw  9615  cofsmo  9680  cfcoflem  9683  coftr  9684  isf32lem2  9765  isf32lem9  9772  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  zorn2lem4  9910  zorn2lem6  9912  zorn2lem7  9913  ttukeylem6  9925  uniimadom  9955  konigthlem  9979  fpwwe2lem8  10048  tskord  10191  tskcard  10192  grupr  10208  gruiin  10221  grudomon  10228  grur1a  10230  genpn0  10414  genpcd  10417  distrlem5pr  10438  psslinpr  10442  ltaddpr  10445  ltexprlem3  10449  ltexprlem6  10452  ltapr  10456  prlem936  10458  suplem1pr  10463  axpre-sup  10580  1re  10630  dedekindle  10793  lemul12a  11487  divgt0  11497  divge0  11498  lbreu  11578  sup2  11584  bndndx  11884  elnnz  11979  nzadd  12018  fzind  12068  fnn0ind  12069  uzwo  12299  lbzbi  12324  zmax  12333  zbtwnre  12334  irradd  12360  irrmul  12361  ledivge1le  12448  xrub  12693  supxrunb2  12701  infmremnf  12724  iccid  12771  uzsubsubfz  12924  fzrevral  12987  elfz0fzfz0  13007  fz0fzelfz0  13008  elfzmlbp  13013  elincfzoext  13090  ssfzoulel  13126  ssfzo12bi  13127  elfzonelfzo  13134  elfznelfzo  13137  elfznelfzob  13138  injresinjlem  13152  fleqceilz  13217  modaddmodup  13297  uzindi  13345  suppssfz  13357  mptnn0fsuppr  13362  le2sq2  13496  sqlecan  13567  facdiv  13643  facwordi  13645  faclbnd  13646  hashimarni  13798  hash2prd  13829  hashle2pr  13831  pr2pwpr  13833  fundmge2nop0  13846  fi1uzind  13851  brfi1indALT  13854  swrdnd2  14008  swrdnnn0nd  14009  swrdnd0  14010  pfxnd0  14041  swrdswrdlem  14057  swrdswrd  14058  ccatopth2  14070  wrd2ind  14076  pfxccatin12lem2a  14080  swrdccatin2  14082  pfxccatin12lem2  14084  pfxccatin12lem3  14085  swrdccat  14088  swrdccat3blem  14092  reuccatpfxs1lem  14099  repswswrd  14137  cshwidxmod  14156  cshwidx0  14159  2cshwcshw  14178  cshwcsh2id  14181  cau3lem  14705  caubnd  14709  climrlim2  14895  rlimcn2  14938  mulcn2  14943  climcau  15018  climbdd  15019  caucvg  15026  modfsummod  15140  p1modz1  15605  dvdsle  15651  dvdsdivcl  15657  ltoddhalfle  15701  halfleoddlt  15702  ndvdssub  15749  gcdcllem1  15837  dvdslegcd  15842  bezoutlem4  15879  dfgcd2  15883  lcmf  15966  lcmfunsnlem1  15970  lcmfunsnlem2lem1  15971  lcmfunsnlem  15974  lcmfdvdsb  15976  lcmfun  15978  coprmdvds1  15985  divgcdcoprm0  15998  cncongr1  16000  cncongr2  16001  prmfac1  16052  pcqcl  16182  dvdsprmpweqle  16211  oddprmdvds  16228  prmpwdvds  16229  infpnlem1  16235  prmgaplem5  16380  prmgaplem6  16381  prmgaplem7  16382  cshwshashlem1  16420  cictr  17066  initoeu2lem1  17265  initoeu2  17267  clatleglb  17727  lidrididd  17871  mulgaddcom  18242  mulginvcom  18243  cycsubm  18336  cyccom  18337  gsmsymgreqlem2  18550  symggen  18589  psgnunilem4  18616  sylow2blem3  18738  frgpnabllem1  18984  dprddisj2  19152  f1rhm0to0ALT  19487  lmodfopnelem1  19661  lssssr  19716  lss1d  19726  lspsncv0  19909  znrrg  20255  mplcoe5lem  20705  cply1mul  20921  coe1fzgsumdlem  20928  gsummoncoe1  20931  evl1gsumdlem  20978  mamufacex  20994  dmatelnd  21099  scmataddcl  21119  scmatsubcl  21120  scmatmulcl  21121  smatvscl  21127  mavmulsolcl  21154  mdetdiagid  21203  cramerlem3  21292  pmatcoe1fsupp  21304  cpmatacl  21319  cpmatmcllem  21321  mp2pm2mplem4  21412  chpscmat  21445  chfacfisf  21457  chfacfisfcpmat  21458  uniopn  21500  opnnei  21723  neindisj2  21726  restcls  21784  restntr  21785  tgcnp  21856  subbascn  21857  iscnp4  21866  lpcls  21967  cmpsublem  22002  cmpsub  22003  tgcmp  22004  cmpcld  22005  dfconn2  22022  1stcrest  22056  2ndcdisj  22059  1stccnp  22065  comppfsc  22135  kgencn2  22160  txlm  22251  kqreglem1  22344  filin  22457  isfil2  22459  ufilmax  22510  ufileu  22522  filufint  22523  cfinufil  22531  elfm2  22551  rnelfmlem  22555  rnelfm  22556  flimopn  22578  fbflim2  22580  flffbas  22598  fclsnei  22622  flimfnfcls  22631  fclscmp  22633  fcfnei  22638  cnpfcf  22644  alexsubALTlem2  22651  alexsubALTlem3  22652  alexsubALTlem4  22653  alexsubALT  22654  ptcmplem4  22658  qustgplem  22724  tsmsres  22747  tsmsxp  22758  metss  23113  metcnp3  23145  ovoliunnul  24109  ovolicc2lem3  24121  dyadmax  24200  itg2le  24341  bddiblnc  24443  itgcn  24446  ellimc3  24480  lhop1  24615  dvfsumrlim  24632  fta1g  24766  fta1  24902  aalioulem3  24928  aalioulem4  24929  ulmcaulem  24987  ulmcau  24988  logbgcd1irr  25378  xrlimcnp  25552  cxploglim  25561  jensen  25572  lgsqrmodndvds  25935  gausslemma2dlem1a  25947  gausslemma2dlem2  25949  gausslemma2dlem3  25950  lgsquad2lem2  25967  2lgslem1a1  25971  2sqlem6  26005  2sq2  26015  2sqnn  26021  2sqreultblem  26030  brbtwn2  26697  ax5seglem5  26725  axcontlem4  26759  axcontlem10  26765  umgrnloopv  26897  umgrnloop  26899  upgredgpr  26933  numedglnl  26935  usgrausgrb  26960  usgrnloopvALT  26989  usgrnloopALT  26991  usgredg2vlem2  27014  ushgredgedg  27017  ushgredgedgloop  27019  upgrreslem  27092  umgrreslem  27093  nbgr0vtxlem  27143  nbusgrvtxm1  27167  uvtxnbgrvtx  27181  cusgredg  27212  cusgrres  27236  cusgrsize2inds  27241  cusgrfi  27246  fusgrregdegfi  27357  ewlkle  27393  uspgr2wlkeqi  27435  wlklenvclwlkOLD  27443  lfgrwlkprop  27475  lfgrwlknloop  27477  pthdivtx  27516  2pthnloop  27518  upgrwlkdvdelem  27523  upgrspthswlk  27525  usgr2wlkneq  27543  usgr2trlncl  27547  usgr2pthlem  27550  usgr2pth  27551  uspgrn2crct  27592  crctcshwlkn0lem4  27597  crctcshwlkn0lem5  27598  crctcshwlkn0  27605  wlkiswwlks1  27651  wlkiswwlks2  27659  wlkiswwlksupgr2  27661  wwlksnred  27676  wwlksnext  27677  wwlksnextbi  27678  wwlksnextwrd  27681  wwlksnextinj  27683  wwlksnextproplem2  27694  wwlksnextproplem3  27695  wspthsnonn0vne  27701  wspn0  27708  2pthon3v  27727  umgrwwlks2on  27741  elwspths2on  27744  wpthswwlks2on  27745  clwwlk1loop  27771  clwwlkccatlem  27772  umgrclwwlkge2  27774  clwlkclwwlklem2a4  27780  clwlkclwwlklem2a  27781  clwlkclwwlklem3  27784  clwlkclwwlkf1lem3  27789  clwlkclwwlkfo  27792  clwwisshclwwslemlem  27796  erclwwlkeqlen  27802  erclwwlksym  27804  clwwlkf  27830  clwwlknscsh  27845  erclwwlknsym  27853  clwwlknonex2lem2  27891  clwwlknonex2  27892  upgr3v3e3cycl  27963  upgr4cycl4dv4e  27968  eucrctshift  28026  3vfriswmgr  28061  1to2vfriswmgr  28062  1to3vfriswmgr  28063  n4cyclfrgr  28074  4cyclusnfrgr  28075  frgrnbnb  28076  frgrncvvdeqlem8  28089  frgrwopreg  28106  frgr2wwlk1  28112  frgr2wwlkeqm  28114  2clwwlk2clwwlklem  28129  numclwwlk1lem2fo  28141  wlkl0  28150  numclwlk2lem2f  28160  frgrreggt1  28176  frgrreg  28177  frgrregord013  28178  frgrregord13  28179  frgrogt3nreg  28180  eulplig  28266  nmoub3i  28554  ipasslem5  28616  htthlem  28698  ocin  29077  spansneleq  29351  spansnss  29352  elspansn4  29354  h1datomi  29362  nmopub2tALT  29690  nmfnleub2  29707  hstel2  30000  cvnbtwn  30067  spansncv2  30074  dmdmd  30081  dmdbr3  30086  dmdbr4  30087  dmdbr5  30089  mdsl0  30091  mdexchi  30116  cvexchlem  30149  atcv1  30161  atomli  30163  atcvatlem  30166  atcvat2i  30168  chirredi  30175  mdsymlem3  30186  mdsymlem4  30187  sumdmdii  30196  sumdmdlem  30199  cdj1i  30214  ssrelf  30374  f1o3d  30380  fisshasheq  32426  umgr2cycllem  32461  cvxpconn  32563  satfv0  32679  satfsschain  32685  satfrel  32688  satfdm  32690  satfv0fun  32692  sat1el2xp  32700  gonarlem  32715  goalrlem  32717  satffunlem1lem1  32723  satffunlem2lem1  32725  satffunlem2lem2  32727  satffun  32730  mrsubccat  32839  msubvrs  32881  fundmpss  33083  dfon2lem6  33107  dfon2lem8  33109  dfon2lem9  33110  dfon2  33111  trpredrec  33151  soseq  33170  wzel  33185  frr3g  33195  nosepdmlem  33261  nodenselem8  33269  colinearxfr  33610  btwnconn1lem11  33632  lineintmo  33692  trer  33738  elicc3  33739  finminlem  33740  nn0prpwlem  33744  fnessref  33779  neibastop2  33783  fgmin  33792  tailfb  33799  ordcmp  33869  ee7.2aOLD  33883  bj-cbvalimt  34046  bj-ceqsalt0  34285  bj-ceqsalt1  34286  isbasisrelowllem1  34733  isbasisrelowllem2  34734  relowlpssretop  34742  fvineqsneu  34789  fvineqsneq  34790  wl-mo3t  34935  finixpnum  35000  matunitlindflem1  35011  matunitlindflem2  35012  poimirlem26  35041  poimirlem27  35042  poimirlem29  35044  ftc1anc  35096  fdc  35141  heibor1lem  35205  ghomco  35287  rngoueqz  35336  unichnidl  35427  dmncan1  35472  ax12indn  36197  lshpdisj  36241  lub0N  36443  glb0N  36447  leat2  36548  hlrelat2  36657  cvrexchlem  36673  cvratlem  36675  atcvrj0  36682  cvrat2  36683  snatpsubN  37004  linepsubN  37006  pmaple  37015  pmapsub  37022  elpaddn0  37054  paddasslem5  37078  trlval2  37417  cdlemn11pre  38464  dihord2pre  38479  mapdordlem2  38891  fsuppind  39403  pell1qrgap  39745  dford3lem1  39897  hbtlem5  40002  ntrneiiso  40727  sbiota1  41072  19.41rg  41190  ee223  41274  or2expropbilem1  43563  funressnfv  43574  2reuimp  43610  f1oresf1o2  43786  zm1nn  43798  nltle2tri  43809  el1fzopredsuc  43821  fzoopth  43823  elsetpreimafvssdm  43842  imasetpreimafvbijlemf1  43860  iccpartlt  43880  iccpartgt  43883  iccelpart  43889  icceuelpart  43892  iccpartnel  43894  fargshiftfo  43898  fargshiftfva  43899  lswn0  43900  ich2exprop  43927  prsprel  43943  sprsymrelfolem2  43949  sprsymrelfo  43953  poprelb  43980  reuopreuprim  43982  goldbachthlem2  44002  odz2prm2pw  44019  fmtnoprmfac1  44021  fmtnofac2lem  44024  prmdvdsfmtnof1lem2  44041  2pwp1prm  44045  sfprmdvdsmersenne  44060  lighneallem3  44064  requad01  44078  requad2  44080  even3prm2  44176  fppr2odd  44188  fpprwpprb  44197  gbegt5  44218  sbgoldbwt  44234  sbgoldbalt  44238  sbgoldbm  44241  bgoldbtbndlem2  44263  bgoldbtbndlem3  44264  bgoldbtbndlem4  44265  bgoldbtbnd  44266  tgblthelfgott  44272  tgoldbach  44274  isomuspgrlem2b  44286  isomuspgrlem2d  44288  isomuspgr  44291  isomgrsym  44293  upgrwlkupwlk  44307  lmod0rng  44431  nzerooringczr  44635  ztprmneprm  44688  ply1mulgsumlem1  44733  ply1mulgsumlem2  44734  lcoel0  44776  linindslinci  44796  lindslinindimp2lem4  44809  lindslinindsimp2lem5  44810  snlindsntor  44819  ldepspr  44821  lincresunit2  44826  fllog2  44921  dignn0ldlem  44955  dignn0flhalflem1  44968  nn0sumshdiglemA  44972  nn0sumshdiglemB  44973  itcovalt2  45030  resum2sqorgt0  45062  eenglngeehlnmlem2  45091  rrx2linest  45095  itscnhlc0xyqsol  45118  itsclc0  45124  setrec1lem2  45157  aacllem  45268
  Copyright terms: Public domain W3C validator