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  413  expcomd  418  impancom  453  a2and  844  dedlem0b  1044  sbequ1  2241  moexexlem  2627  ralrimdvva  3204  ceqsalt  3476  vtoclgft  3510  sbciegft  3778  reupick  4279  reusv3  5361  sbcop1  5446  propeqop  5465  pwssun  5529  wefrc  5628  ssrel  5739  ssrelOLD  5740  ssrel2  5742  ssrelrel  5753  ssrelrn  5851  tz7.7  6344  ordtr2  6362  onmindif  6410  unizlim  6441  funssres  6546  f1ssf1  6817  fvmptt  6969  fveqdmss  7030  fvcofneq  7044  funsndifnop  7098  funfvima2  7182  isoini  7284  isopolem  7291  weniso  7300  f1ocnv2d  7607  limsssuc  7787  tfindsg  7798  limomss  7808  findsg  7837  funcnvuni  7869  f1oweALT  7906  funelss  7980  bropopvvv  8023  bropfvvvvlem  8024  bropfvvvv  8025  f1o2ndf1  8055  frxp  8059  soseq  8092  suppfnss  8121  wfrlem12OLD  8267  onfununi  8288  tz7.49  8392  omordi  8514  omlimcl  8526  omass  8528  oeordsuc  8542  nnmordi  8579  nnmord  8580  omabs  8598  xpdom2  9012  infensuc  9100  findcard2  9109  findcard2d  9111  findcard2OLD  9229  findcard3  9230  findcard3OLD  9231  frfi  9233  xpfiOLD  9263  fsuppres  9331  dffi2  9360  elfiun  9367  ordiso2  9452  ordtypelem7  9461  suc11reg  9556  inf3lem2  9566  noinfep  9597  cantnfle  9608  cantnflem1  9626  cantnf  9630  ttrclss  9657  trcl  9665  epfrs  9668  frr3g  9693  r1sdom  9711  updjud  9871  pr2neOLD  9942  dfac8alem  9966  indcardi  9978  alephordi  10011  dfac12lem3  10082  pwsdompw  10141  cofsmo  10206  cfcoflem  10209  coftr  10210  isf32lem2  10291  isf32lem9  10298  axcc3  10375  domtriomlem  10379  axdc3lem2  10388  axdc3lem4  10390  zorn2lem4  10436  zorn2lem6  10438  zorn2lem7  10439  ttukeylem6  10451  uniimadom  10481  konigthlem  10505  fpwwe2lem7  10574  tskord  10717  tskcard  10718  grupr  10734  gruiin  10747  grudomon  10754  grur1a  10756  genpn0  10940  genpcd  10943  distrlem5pr  10964  psslinpr  10968  ltaddpr  10971  ltexprlem3  10975  ltexprlem6  10978  ltapr  10982  prlem936  10984  suplem1pr  10989  axpre-sup  11106  1re  11156  dedekindle  11320  lemul12a  12014  divgt0  12024  divge0  12025  lbreu  12106  sup2  12112  bndndx  12413  elnnz  12510  nzadd  12552  fzind  12602  fnn0ind  12603  uzwo  12837  lbzbi  12862  zmax  12871  zbtwnre  12872  irradd  12899  irrmul  12900  ledivge1le  12987  xrub  13232  supxrunb2  13240  infmremnf  13263  iccid  13310  uzsubsubfz  13464  fzrevral  13527  elfz0fzfz0  13547  fz0fzelfz0  13548  elfzmlbp  13553  elincfzoext  13631  ssfzoulel  13667  ssfzo12bi  13668  elfzonelfzo  13675  elfznelfzo  13678  elfznelfzob  13679  injresinjlem  13693  fleqceilz  13760  modaddmodup  13840  uzindi  13888  suppssfz  13900  mptnn0fsuppr  13905  le2sq2  14041  sqlecan  14114  facdiv  14188  facwordi  14190  faclbnd  14191  hashimarni  14342  hash2prd  14375  hashle2pr  14377  pr2pwpr  14379  fundmge2nop0  14392  fi1uzind  14397  brfi1indALT  14400  swrdnd2  14544  swrdnnn0nd  14545  swrdnd0  14546  pfxnd0  14577  swrdswrdlem  14593  swrdswrd  14594  ccatopth2  14606  wrd2ind  14612  pfxccatin12lem2a  14616  swrdccatin2  14618  pfxccatin12lem2  14620  pfxccatin12lem3  14621  swrdccat  14624  swrdccat3blem  14628  reuccatpfxs1lem  14635  repswswrd  14673  cshwidxmod  14692  cshwidx0  14695  2cshwcshw  14715  cshwcsh2id  14718  cau3lem  15240  caubnd  15244  climrlim2  15430  rlimcn3  15473  mulcn2  15479  climcau  15556  climbdd  15557  caucvg  15564  modfsummod  15680  p1modz1  16144  dvdsle  16193  dvdsdivcl  16199  ltoddhalfle  16244  halfleoddlt  16245  ndvdssub  16292  gcdcllem1  16380  dvdslegcd  16385  bezoutlem4  16424  dfgcd2  16428  lcmf  16510  lcmfunsnlem1  16514  lcmfunsnlem2lem1  16515  lcmfunsnlem  16518  lcmfdvdsb  16520  lcmfun  16522  coprmdvds1  16529  divgcdcoprm0  16542  cncongr1  16544  cncongr2  16545  prmfac1  16598  pcqcl  16729  dvdsprmpweqle  16759  oddprmdvds  16776  prmpwdvds  16777  infpnlem1  16783  prmgaplem5  16928  prmgaplem6  16929  prmgaplem7  16930  cshwshashlem1  16969  cictr  17689  initoeu2lem1  17901  initoeu2  17903  clatleglb  18408  lidrididd  18526  mulgaddcom  18901  mulginvcom  18902  cycsubm  18996  cyccom  18997  gsmsymgreqlem2  19214  symggen  19253  psgnunilem4  19280  sylow2blem3  19405  frgpnabllem1  19652  dprddisj2  19819  f1rhm0to0ALT  20176  lmodfopnelem1  20361  lssssr  20417  lss1d  20427  lspsncv0  20610  znrrg  20975  mplcoe5lem  21443  cply1mul  21668  coe1fzgsumdlem  21675  gsummoncoe1  21678  evl1gsumdlem  21725  mamufacex  21741  dmatelnd  21848  scmataddcl  21868  scmatsubcl  21869  scmatmulcl  21870  smatvscl  21876  mavmulsolcl  21903  mdetdiagid  21952  cramerlem3  22041  pmatcoe1fsupp  22053  cpmatacl  22068  cpmatmcllem  22070  mp2pm2mplem4  22161  chpscmat  22194  chfacfisf  22206  chfacfisfcpmat  22207  uniopn  22249  opnnei  22474  neindisj2  22477  restcls  22535  restntr  22536  tgcnp  22607  subbascn  22608  iscnp4  22617  lpcls  22718  cmpsublem  22753  cmpsub  22754  tgcmp  22755  cmpcld  22756  dfconn2  22773  1stcrest  22807  2ndcdisj  22810  1stccnp  22816  comppfsc  22886  kgencn2  22911  txlm  23002  kqreglem1  23095  filin  23208  isfil2  23210  ufilmax  23261  ufileu  23273  filufint  23274  cfinufil  23282  elfm2  23302  rnelfmlem  23306  rnelfm  23307  flimopn  23329  fbflim2  23331  flffbas  23349  fclsnei  23373  flimfnfcls  23382  fclscmp  23384  fcfnei  23389  cnpfcf  23395  alexsubALTlem2  23402  alexsubALTlem3  23403  alexsubALTlem4  23404  alexsubALT  23405  ptcmplem4  23409  qustgplem  23475  tsmsres  23498  tsmsxp  23509  metss  23867  metcnp3  23899  ovoliunnul  24874  ovolicc2lem3  24886  dyadmax  24965  itg2le  25107  bddiblnc  25209  itgcn  25212  ellimc3  25246  lhop1  25381  dvfsumrlim  25398  fta1g  25535  fta1  25671  aalioulem3  25697  aalioulem4  25698  ulmcaulem  25756  ulmcau  25757  logbgcd1irr  26147  xrlimcnp  26321  cxploglim  26330  jensen  26341  lgsqrmodndvds  26704  gausslemma2dlem1a  26716  gausslemma2dlem2  26718  gausslemma2dlem3  26719  lgsquad2lem2  26736  2lgslem1a1  26740  2sqlem6  26774  2sq2  26784  2sqnn  26790  2sqreultblem  26799  nosepdmlem  27034  nodenselem8  27042  madebdaylemlrcut  27231  addsprop  27291  addsunif  27313  negsprop  27336  brbtwn2  27857  ax5seglem5  27885  axcontlem4  27919  axcontlem10  27925  umgrnloopv  28060  umgrnloop  28062  upgredgpr  28096  numedglnl  28098  usgrausgrb  28123  usgrnloopvALT  28152  usgrnloopALT  28154  usgredg2vlem2  28177  ushgredgedg  28180  ushgredgedgloop  28182  upgrreslem  28255  umgrreslem  28256  nbgr0vtxlem  28306  nbusgrvtxm1  28330  uvtxnbgrvtx  28344  cusgredg  28375  cusgrres  28399  cusgrsize2inds  28404  cusgrfi  28409  fusgrregdegfi  28520  ewlkle  28556  uspgr2wlkeqi  28599  lfgrwlkprop  28638  lfgrwlknloop  28640  pthdivtx  28680  2pthnloop  28682  upgrwlkdvdelem  28687  upgrspthswlk  28689  usgr2wlkneq  28707  usgr2trlncl  28711  usgr2pthlem  28714  usgr2pth  28715  uspgrn2crct  28756  crctcshwlkn0lem4  28761  crctcshwlkn0lem5  28762  crctcshwlkn0  28769  wlkiswwlks1  28815  wlkiswwlks2  28823  wlkiswwlksupgr2  28825  wwlksnred  28840  wwlksnext  28841  wwlksnextbi  28842  wwlksnextwrd  28845  wwlksnextinj  28847  wwlksnextproplem2  28858  wwlksnextproplem3  28859  wspthsnonn0vne  28865  wspn0  28872  2pthon3v  28891  umgrwwlks2on  28905  elwspths2on  28908  wpthswwlks2on  28909  clwwlk1loop  28935  clwwlkccatlem  28936  umgrclwwlkge2  28938  clwlkclwwlklem2a4  28944  clwlkclwwlklem2a  28945  clwlkclwwlklem3  28948  clwlkclwwlkf1lem3  28953  clwlkclwwlkfo  28956  clwwisshclwwslemlem  28960  erclwwlkeqlen  28966  erclwwlksym  28968  clwwlkf  28994  clwwlknscsh  29009  erclwwlknsym  29017  clwwlknonex2lem2  29055  clwwlknonex2  29056  upgr3v3e3cycl  29127  upgr4cycl4dv4e  29132  eucrctshift  29190  3vfriswmgr  29225  1to2vfriswmgr  29226  1to3vfriswmgr  29227  n4cyclfrgr  29238  4cyclusnfrgr  29239  frgrnbnb  29240  frgrncvvdeqlem8  29253  frgrwopreg  29270  frgr2wwlk1  29276  frgr2wwlkeqm  29278  2clwwlk2clwwlklem  29293  numclwwlk1lem2fo  29305  wlkl0  29314  numclwlk2lem2f  29324  frgrreggt1  29340  frgrreg  29341  frgrregord013  29342  frgrregord13  29343  frgrogt3nreg  29344  eulplig  29430  nmoub3i  29718  ipasslem5  29780  htthlem  29862  ocin  30241  spansneleq  30515  spansnss  30516  elspansn4  30518  h1datomi  30526  nmopub2tALT  30854  nmfnleub2  30871  hstel2  31164  cvnbtwn  31231  spansncv2  31238  dmdmd  31245  dmdbr3  31250  dmdbr4  31251  dmdbr5  31253  mdsl0  31255  mdexchi  31280  cvexchlem  31313  atcv1  31325  atomli  31327  atcvatlem  31330  atcvat2i  31332  chirredi  31339  mdsymlem3  31350  mdsymlem4  31351  sumdmdii  31360  sumdmdlem  31363  cdj1i  31378  ssrelf  31537  f1o3d  31544  fisshasheq  33708  umgr2cycllem  33737  cvxpconn  33839  satfv0  33955  satfsschain  33961  satfrel  33964  satfdm  33966  satfv0fun  33968  sat1el2xp  33976  gonarlem  33991  goalrlem  33993  satffunlem1lem1  33999  satffunlem2lem1  34001  satffunlem2lem2  34003  satffun  34006  mrsubccat  34115  msubvrs  34157  fundmpss  34344  dfon2lem6  34366  dfon2lem8  34368  dfon2lem9  34369  dfon2  34370  wzel  34402  colinearxfr  34663  btwnconn1lem11  34685  lineintmo  34745  trer  34791  elicc3  34792  finminlem  34793  nn0prpwlem  34797  fnessref  34832  neibastop2  34836  fgmin  34845  tailfb  34852  ordcmp  34922  ee7.2aOLD  34936  bj-cbvalimt  35106  bj-ceqsalt0  35354  bj-ceqsalt1  35355  isbasisrelowllem1  35829  isbasisrelowllem2  35830  relowlpssretop  35838  fvineqsneu  35885  fvineqsneq  35886  wl-mo3t  36034  finixpnum  36066  matunitlindflem1  36077  matunitlindflem2  36078  poimirlem26  36107  poimirlem27  36108  poimirlem29  36110  ftc1anc  36162  fdc  36207  heibor1lem  36271  ghomco  36353  rngoueqz  36402  unichnidl  36493  dmncan1  36538  ax12indn  37408  lshpdisj  37452  lub0N  37654  glb0N  37658  leat2  37759  hlrelat2  37869  cvrexchlem  37885  cvratlem  37887  atcvrj0  37894  cvrat2  37895  snatpsubN  38216  linepsubN  38218  pmaple  38227  pmapsub  38234  elpaddn0  38266  paddasslem5  38290  trlval2  38629  cdlemn11pre  39676  dihord2pre  39691  mapdordlem2  40103  fsuppind  40768  sn-sup2  40941  pell1qrgap  41200  dford3lem1  41353  hbtlem5  41458  onexlimgt  41580  onsucf1olem  41608  omcl2  41669  ntrneiiso  42370  sbiota1  42721  19.41rg  42839  ee223  42923  or2expropbilem1  45273  funressnfv  45284  fcoresf1  45310  2reuimp  45354  f1oresf1o2  45530  zm1nn  45541  nltle2tri  45552  el1fzopredsuc  45564  fzoopth  45566  elsetpreimafvssdm  45585  imasetpreimafvbijlemf1  45603  iccpartlt  45623  iccpartgt  45626  iccelpart  45632  icceuelpart  45635  iccpartnel  45637  fargshiftfo  45641  fargshiftfva  45642  lswn0  45643  ich2exprop  45670  prsprel  45686  sprsymrelfolem2  45692  sprsymrelfo  45696  poprelb  45723  reuopreuprim  45725  goldbachthlem2  45745  odz2prm2pw  45762  fmtnoprmfac1  45764  fmtnofac2lem  45767  prmdvdsfmtnof1lem2  45784  2pwp1prm  45788  sfprmdvdsmersenne  45802  lighneallem3  45806  requad01  45820  requad2  45822  even3prm2  45918  fppr2odd  45930  fpprwpprb  45939  gbegt5  45960  sbgoldbwt  45976  sbgoldbalt  45980  sbgoldbm  45983  bgoldbtbndlem2  46005  bgoldbtbndlem3  46006  bgoldbtbndlem4  46007  bgoldbtbnd  46008  tgblthelfgott  46014  tgoldbach  46016  isomuspgrlem2b  46028  isomuspgrlem2d  46030  isomuspgr  46033  isomgrsym  46035  upgrwlkupwlk  46049  lmod0rng  46173  nzerooringczr  46377  ztprmneprm  46430  ply1mulgsumlem1  46474  ply1mulgsumlem2  46475  lcoel0  46516  linindslinci  46536  lindslinindimp2lem4  46549  lindslinindsimp2lem5  46550  snlindsntor  46559  ldepspr  46561  lincresunit2  46566  fllog2  46661  dignn0ldlem  46695  dignn0flhalflem1  46708  nn0sumshdiglemA  46712  nn0sumshdiglemB  46713  itcovalt2  46770  resum2sqorgt0  46802  eenglngeehlnmlem2  46831  rrx2linest  46835  itscnhlc0xyqsol  46858  itsclc0  46864  setrec1lem2  47140  aacllem  47255
  Copyright terms: Public domain W3C validator