MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impcom Structured version   Unicode version

Theorem impcom 420
Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
imp.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
impcom  |-  ( ( ps  /\  ph )  ->  ch )

Proof of Theorem impcom
StepHypRef Expression
1 imp.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21com12 29 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 419 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpan9  456  equtr2  1700  19.41  1900  19.41OLD  1901  dvelimfOLD  2069  equvini  2083  nfsb4t  2127  ax11eq  2270  ax11el  2271  mopick  2343  2euex  2353  gencl  2984  2gencl  2985  rspccva  3051  sbcimdv  3222  sseq0  3659  minel  3683  r19.2z  3717  elelpwi  3809  ssuni  4037  disji2  4199  disjiun  4202  trint0  4319  ssexg  4349  pofun  4519  solin  4526  2optocl  4953  3optocl  4954  elrnmpt1  5119  resieq  5156  funimaexg  5530  fnun  5551  fss  5599  fun  5607  dmfex  5626  fvelimab  5782  fvmptss  5813  fmptco  5901  fnressn  5918  fressnfv  5920  fvtp2g  5943  fvtp3g  5944  fnex  5961  funfvima3  5975  isores3  6055  f1o2ndf1  6454  frxp  6456  fnse  6463  mpt2xopxnop0  6466  reldmtpos  6487  smores  6614  tz7.48-2  6699  tz7.49  6702  oacl  6779  omcl  6780  oecl  6781  oarec  6805  oewordri  6835  oeworde  6836  oelim2  6838  oeoa  6840  oeoelem  6841  oeoe  6842  nnacl  6854  nnmcl  6855  nnecl  6856  nnmsucr  6868  2ecoptocl  6995  undifixp  7098  xpf1o  7269  limensuc  7284  ac6sfi  7351  frfi  7352  difinf  7377  elfiun  7435  dffi3  7436  xpwdomg  7553  preleq  7572  infdiffi  7612  epfrs  7667  rankxpsuc  7806  tskwe  7837  infxpenlem  7895  fseqenlem1  7905  kmlem2  8031  cff1  8138  cflim2  8143  sornom  8157  infpssrlem4  8186  fin23lem26  8205  fin23lem30  8222  fin23lem34  8226  isf32lem11  8243  fin67  8275  isfin7-2  8276  fin1a2lem10  8289  axcc2lem  8316  axdc2lem  8328  axdc3lem2  8331  axdc3lem4  8333  axdc4lem  8335  iunfo  8414  tsk0  8638  gruina  8693  grur1a  8694  mulcanenq  8837  reclem2pr  8925  supsrlem  8986  supsr  8987  ax1rid  9036  mulgt1  9869  lbreu  9958  nnaddcl  10022  nnmulcl  10023  nn0n0n1ge2b  10281  fzind  10368  fnn0ind  10369  uzaddcl  10533  xmulasslem2  10861  supxrunb1  10898  supxrunb2  10899  elfznelfzob  11193  injresinjlem  11199  injresinj  11200  om2uzlti  11290  fsequb  11314  ser1const  11379  expcllem  11392  expeq0  11410  faclbnd  11581  faclbnd6  11590  hasheqf1oi  11635  hashf1rn  11636  hashgadd  11651  hashunx  11660  hashnn0n0nn  11664  hashgt0elex  11670  hash2prb  11689  hashxp  11697  seqcoll  11712  brfi1indlem  11714  brfi1uzind  11715  cjexp  11955  absexp  12109  r19.29uz  12154  caubnd  12162  sqreu  12164  climshft  12370  climub  12455  climserle  12456  sumss  12518  sumss2  12520  o1fsum  12592  binom  12609  bcxmas  12615  climcndslem1  12629  climcndslem2  12630  cvgrat  12660  demoivreALT  12802  znnenlem  12811  ruclem8  12836  dvdsfac  12904  smu01lem  12997  dvdslegcd  13016  gcdneg  13026  gcdmultiple  13050  seq1st  13062  alginv  13066  prmdvdsexp  13114  lubss  14548  lubel  14549  frmdgsum  14807  gaass  15074  gsumwrev  15162  cnfldmulg  16733  cnfldexp  16734  clsss  17118  ntrss  17119  restntr  17246  cmpsublem  17462  cmpsub  17463  bwth  17473  2ndcrest  17517  txindislem  17665  t0kq  17850  filufint  17952  fbflim2  18009  flftg  18028  alexsubALTlem4  18081  cnextfvval  18096  tmdmulg  18122  ustuqtop4  18274  xmettri2  18370  mettri  18382  metss  18538  lmmbr  19211  caublcls  19261  lmcau  19265  ovolunlem1a  19392  nulmbl2  19431  voliunlem1  19444  iunmbl  19447  volsup  19450  dvlip  19877  dvfsumle  19905  pf1ind  19975  degltlem1  19995  ply1divex  20059  plyco  20160  dvnply2  20204  plydivex  20214  aannenlem2  20246  aaliou3lem2  20260  ulmcau  20311  dchrisumlem1  21183  dchrisumlem2  21184  dchrisumlem3  21185  qabvle  21319  ostthlem2  21322  ostth2lem2  21328  usgra2edg  21402  usgraedg4  21406  usgraidx2vlem2  21411  nbusgra  21440  nbgraf1olem5  21455  nb3graprlem1  21460  nb3graprlem2  21461  cusgrarn  21468  nbcusgra  21472  cusgrasize2inds  21486  sizeusglecusglem1  21493  uvtxnbgra  21502  usgrnloop  21563  redwlk  21606  wlkdvspthlem  21607  fargshiftf1  21624  usgrcyclnl1  21627  usgrcyclnl2  21628  nvnencycllem  21630  constr3trllem2  21638  isgrpo  21784  opidon  21910  grpomndo  21934  vcdi  22031  vcdir  22032  vcass  22033  nmosetre  22265  hlim2  22694  shscli  22819  chintcli  22833  dfch2  22909  spansncvi  23154  nmopsetretALT  23366  nmfnsetre  23380  lnopl  23417  lnfnl  23434  pjss2coi  23667  pjorthcoi  23672  pjscji  23673  pjssdif2i  23677  pjclem4a  23701  pj3lem1  23709  strlem5  23758  hstrlem5  23766  cvmdi  23827  mdslmd3i  23835  atcv1  23883  atcvat4i  23900  cdj3lem2a  23939  cdj3lem3a  23942  iuninc  24011  disji2f  24019  disjif2  24023  fmptcof2  24076  ssct  24101  xrsmulgzz  24200  ofldchr  24244  esumfzf  24459  issgon  24506  voliune  24585  volfiniune  24586  rrvsum  24712  cvmliftlem15  24985  relexprel  25134  relexpfld  25137  relexpadd  25138  relexpindlem  25139  rtrclreclem.trans  25146  rtrclreclem.min  25147  clim2prod  25216  prodfn0  25222  prodfrec  25223  ntrivcvgfvn0  25227  fprodefsum  25298  fprodn0  25303  fprod2dlem  25304  iprodefisumlem  25317  faclimlem1  25362  dfon2lem6  25415  tfisg  25479  poseq  25528  wfrlem11  25548  wfrlem12  25549  frrlem4  25585  frrlem5c  25588  frrlem11  25594  nodenselem5  25640  nocvxminlem  25645  nocvxmin  25646  axeuclidlem  25901  idinside  26018  onsucconi  26187  wl-aleq  26235  itg2addnclem  26256  nn0prpw  26326  upixp  26431  welb  26438  sdclem2  26446  metf1o  26461  sstotbnd3  26485  isbndx  26491  ismtycnv  26511  heiborlem4  26523  bfplem1  26531  mzpexpmpt  26802  diophren  26874  expmordi  27010  rmxypos  27012  jm2.17a  27025  jm2.17b  27026  rmygeid  27029  divalgmodcl  27058  jm2.18  27059  jm2.25  27070  jm2.15nn0  27074  jm2.16nn0  27075  pwslnm  27173  isnumbasgrplem1  27243  dgrnznn  27317  dgraalem  27327  symggen  27388  2reurex  27935  2reu1  27940  eu2ndop1stv  27956  afvfv0bi  27992  afveu  27993  afvres  28012  aovmpt4g  28041  ndmaovass  28046  ndmaovdistr  28047  imarnf1pr  28084  elfzmlbm  28106  elfzmlbp  28107  elfzelfzelfz  28109  fz0fzdiffz0  28119  ubmelfzo  28126  ubmelm1fzo  28127  subsubelfzo0  28135  fzofzim  28136  fzoopth  28139  2ffzoeq  28140  hashimarni  28164  ccatsymb  28179  swrd0  28183  swrdvalodm2  28188  swrd0swrd  28197  swrdswrdlem  28198  swrdswrd  28199  swrdccatfn  28204  swrdccatin1  28205  swrdccatin12lem3a  28208  swrdccatin2  28210  swrdccatin12lem3  28212  swrdccatin12lem4  28213  swrdccatin12  28214  swrdccat3  28215  swrdccat  28216  swrdccat3blem  28218  cshwidx  28242  2cshwmod  28257  cshweqdif2  28270  cshweqdif2s  28271  cshweqrep  28274  cshw1  28275  cshwsame0  28278  cshwssizelem1a  28279  cshwssizelem2  28281  iswlkg  28300  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2wlkspthlem2  28307  usgra2wlkspth  28308  usgra2pth  28311  el2wlkonot  28336  el2spthonot  28337  el2wlkonotot0  28339  usg2wlkonot  28350  usg2wotspth  28351  usg2spthonot0  28356  usgrauvtxvd  28363  frgra1v  28388  1to2vfriswmgra  28396  1to3vfriswmgra  28397  3cyclfrgrarn1  28402  4cycl2vnunb  28407  frgrancvvdeqlem3  28421  frgrawopreglem3  28435  frgrawopreglem4  28436  frgrawopreg  28438  frg2woteqm  28448  2spotdisj  28450  2spotiundisj  28451  usg2spot2nb  28454  sspwimpcf  29032  sspwimpcfVD  29033  e2ebindALT  29041  bnj228  29102  bnj926  29138  bnj1294  29189  bnj229  29255  bnj607  29287  bnj908  29302  bnj953  29310  bnj1118  29353  bnj1174  29372  bnj1388  29402  dvelimfOLD7  29727  cvrat4  30240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator