HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ex 373
Description: Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) (The proof was shortened by Eric Schmidt, 22-Dec-2006.)
Hypothesis
Ref Expression
exp.1 |- ((ph /\ ps) -> ch)
Assertion
Ref Expression
ex |- (ph -> (ps -> ch))
Proof of Theorem ex
StepHypRef Expression
1 exp.1 . 2 |- ((ph /\ ps) -> ch)
2 impexp 347 . 2 |- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))
31, 2mpbi 189 1 |- (ph -> (ps -> ch))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  expcom 374  exp31 376  exp32 377  exp4b 379  exp41 382  exp43 384  adantll 392  adantlr 393  adantrl 394  adantrr 395  jaoian 425  jaodan 426  anidms 434  sylan 448  sylan2 451  syldan 467  sylanc 471  pm2.61ian 475  pm2.61dan 476  condan 477  anabss7 502  impbida 517  3imtr3g 550  pm5.74da 584  ibib 588  jcad 598  pm5.32da 647  pm5.21nd 678  mpan 693  mpan2 694  mpdan 702  mpanl1 704  mpanl2 705  mpanr1 707  mpanr2 708  mpanlr1 709  nbn2 719  ecase3 750  ecase 751  3adantl1 801  3adantl2 802  3adantl3 803  3jcad 818  3impia 828  3an1rs 843  3exp1 847  3exp2 849  syl3anl1 870  syl3anl2 871  syl3anl3 872  3jaoian 886  3jaodan 887  mp3anl1 907  mp3anl2 908  mp3anl3 909  19.21ad 1055  equs4 1146  dvelimfALT 1149  a4imed 1157  sbequ1 1174  ax11v2 1210  sbequi 1223  hbsb4 1243  dvelimdf 1246  sbcom 1253  sbcom2 1329  sbal1 1341  ax11indi 1360  ax11inda 1364  a12stdy4 1368  a12lem1 1369  a12study 1371  a12studyALT 1372  euor2 1430  moexex 1431  rgen2a 1691  r19.20ia 1697  r19.20da 1700  r19.21aiva 1706  r19.21adva 1711  r19.21advv 1713  r19.21advva 1714  r19.22dva 1731  r19.23aiva 1736  r19.23adva 1739  2gencl 1820  vtocl2ga 1844  vtocl3ga 1845  rcla4edv 1870  ceqex 1877  reu3 1921  sspss 2135  sspsstr 2141  psssstr 2142  neldif 2155  reuss2 2265  reupick 2269  ssne0 2295  disjne 2305  pssdifn0 2319  sspr 2466  prel12 2475  intssuni 2545  ssiun2 2583  opabsb 2804  pwssun 2816  sotrieq 2852  reuuni2f 2873  ralxfrd 2887  iunpw 2904  efrirr 2918  dfwe2 2925  wefrc 2933  ordelord 2960  tz7.7 2963  ordsseleq 2966  onfr 2976  ordon 2977  ssorduni 2983  ordtr2 2992  ordunidif 2995  onint 2996  onint0 2997  onintss 3001  oninton 3002  onnminsb 3006  oneqmini 3007  oneqmin 3008  onminex 3010  ordsssuc2 3049  onmindif2 3051  ordsuc 3055  ordpwsuc 3056  ordsucelsuc 3063  ordtri2or2 3068  ordsucun 3072  onsucuni2 3081  nlimsucg 3102  unizlim 3103  ordunisuc2 3105  limsuc 3110  limsssuc 3111  tfi 3116  dfom2 3123  limomss 3127  limom 3136  peano5 3143  nn0suc 3144  findsg 3147  tfinds 3151  tfindsg 3152  tfindsg2 3153  2optocl 3226  relop 3265  relimasn 3409  dffun7 3526  imadif 3560  2elresin 3584  funrnex 3599  zfrep6 3600  fnopabg 3601  fcoi1 3630  fcoi2 3631  feu 3632  fcnvres 3633  f1oun 3691  f1dmex 3695  funbrfv 3735  fnopabfv 3743  dfimafn 3746  funimass4 3748  ssimaex 3753  funfv 3755  fvco 3759  fvco2 3760  fvopabn 3771  eqfnfv 3782  fvimacnv 3790  funimass3 3791  dff2 3802  dffo4 3805  dffo5 3806  fopab2 3808  fopabco 3817  fsn 3819  fconst5 3833  funfvima 3837  funfvima2 3838  funiunfv 3851  isotr 3882  isotrALT 3883  isomin 3884  isofrlem 3886  tfrlem1 3896  tfrlem5 3900  tfrlem9 3904  tfrlem11 3906  rdgsucopabn 3932  rdglim2 3934  tz7.48-2 3942  tz7.48-3 3943  abianfplem 3946  abianfp 3947  ndmoprcl 4030  oe0lem 4136  oevn0 4138  omcl 4155  oecl 4156  oa0r 4157  om1r 4161  oe1m 4163  oaordi 4164  oawordex 4175  oaordex 4176  oaass 4179  omordi 4181  omord 4183  omcan 4184  omwordi 4186  om00 4190  omlimcl 4193  odi 4194  omass 4195  oneo 4196  oen0 4197  oeordi 4198  oecan 4200  oewordi 4202  oewordri 4203  oeworde 4204  oeordsuc 4205  oelim2 4206  nnmcom 4225  nnmordi 4230  oaabs 4236  nneob 4239  erthi 4265  erdisj 4270  2ecoptocl 4288  brecop 4290  th3qlem1 4298  breng 4357  brdomg 4358  dom2d 4385  ensymg 4392  fundmen 4409  undom 4418  xpdom2 4422  pw2en 4426  sbthlem1 4427  sdomnsym 4442  sdomdomtr 4449  ensdomtr 4451  domsdomtr 4456  enen1 4457  enen2 4458  domen1 4459  domen2 4460  sdomen1 4461  fodomr 4463  mapenlem2 4470  mapen 4471  mapdom2 4474  mapunen 4482  ssenen 4484  phplem4 4491  nneneq 4492  php 4493  php3 4495  onomeneq 4498  nndomo 4500  pssinf 4507  pssnn 4513  ssfi 4515  unblem2 4518  unblem3 4519  isfinite2 4523  unfi 4528  fiint 4534  fodomfi 4540  fodomfib 4541  iunfi 4543  pm54.43 4546  supnub 4556  suppr 4562  supsnALT 4564  suc11reg 4577  inf3lem1 4585  inf3lem5 4589  inf3lem6 4590  infensuc 4610  noinfep 4612  trcl 4617  zfregs 4619  r1tr 4626  r1ord 4627  r1val1 4630  ssrankr1 4648  r1pwcl 4659  rankonid 4667  rankxplim 4684  rankxplim3 4686  hta 4700  aceq5lem4 4710  aceq5 4712  aceq6b 4714  ac5b 4725  ac6lem 4726  kmlem11 4747  zorn2lem4 4763  zorn2lem6 4765  zorn2lem7 4766  fodomb 4772  brdom6disj 4777  unidom 4780  uniimadom 4782  carddomi 4807  sucdom 4814  sdomsdomcard 4820  cardlim 4823  ondomcard 4829  carduni 4830  cardiun 4831  cardmin 4832  alephon 4837  alephcard 4839  alephnbtwn 4840  alephordi 4846  alephord2i 4849  alephsucdom 4852  cardaleph 4857  cardalephex 4858  cardinfima 4863  alephval2 4874  alephval3 4875  cfub 4880  cflim 4881  axextnd 4915  axrepndlem1 4916  axrepndlem2 4917  axunnd 4920  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axpownd 4925  axregndlem2 4927  axregnd 4928  axinfndlem1 4929  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936  mulcanpi 4999  nlt1pi 5005  indpi 5006  ordpipq 5028  ltexpq 5052  prcdpq 5069  genpnnp 5080  genpcd 5081  1pr 5089  distrlem4pr 5102  distrlem5pr 5103  1idpr 5105  prlem934 5111  ltexprlem2 5115  ltexprlem3 5116  ltexprlem4 5117  ltexprlem7 5120  ltexpri 5121  addcanpr 5124  prlem936b 5126  prlem936 5127  reclem2pr 5129  reclem3pr 5130  reclem4pr 5131  suplem1pr 5133  suplem2pr 5134  ltsrpr 5158  suppsr2 5195  suppsr3 5196  supsrlem2 5198  supsr 5203  cnegextlem1 5317  cnegextlem2 5318  cnegextlem3 5319  negeu 5327  addsubt 5356  1re 5407  0re 5412  letrt 5498  xrlttrit 5525  xrletrt 5537  addgegt0 5574  recext 5657  mulcan2t 5662  receu 5670  div23t 5705  div13t 5706  div12t 5707  divadddivt 5740  prodge0 5776  prodgt02t 5783  prodge02t 5785  ltmul2 5790  lemul1 5791  lemul2 5792  lemul1it 5793  lemul1itOLD 5794  lemul12ait 5798  lemul12itOLD 5799  lemul12it 5800  mulgt1t 5801  lediv1t 5806  ltmuldiv2t 5818  ltdivmult 5819  ledivmult 5820  lemuldiv2t 5825  ltdiv2t 5835  ledivp1 5854  ltdivp1 5855  nnrecgt0t 5900  nominpos 5990  lbreu 5992  sup2 5998  suprleub 6006  infmsup 6015  infmrcl 6016  xrsupexmnf 6021  xrinfmexpnf 6022  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxrre 6030  supxrpnf 6035  supxrunb1 6036  supxrunb2 6037  supxrbnd 6038  supxrleub 6046  lt0nnn0 6063  nn0ge0t 6064  nnnn0addclt 6072  elnnz 6092  nn0subt 6108  zaddclt 6112  zrevaddclt 6117  elnn0nn 6118  zltp1let 6128  zextlet 6136  btwnnzt 6139  peano2uz2 6149  uzind2 6154  uzindOLD 6156  uzwo4OLD 6158  uzwo5OLD 6159  nn0ind-raph 6162  btwnz 6163  uzwo3lem1 6164  zmax 6168  zbtwnre 6169  flval3t 6182  qrecclt 6211  qrevaddclt 6213  qbtwnre 6216  qsqueeze 6218  monoord 6231  seq1lem1 6246  seq1rn2 6258  seq1res 6264  ser1add2 6275  ser1add 6276  seq1shftid 6293  iooval2t 6304  elioo4g 6318  elioc2t 6322  elico2t 6323  elicc2t 6324  uzss 6363  uz11t 6364  eluzp1m1t 6365  uzwo 6387  uzwoOLD 6388  fznt 6425  fzoptht 6434  elfzp1 6442  fzrevralt 6451  fsequb 6455  seqzfveq 6486  seqzrn2 6488  ser0cl1 6496  expp1t 6506  expne0it 6519  expge0t 6522  expgt1t 6523  expwordit 6534  expword2it 6536  expmwordit 6537  exple1t 6538  sqlecant 6572  sq01t 6582  discrlem3 6588  nn0opthlem2 6595  sqr0 6602  sqrlem12 6614  sqr11 6633  sqr2irr 6659  inelr 6665  crulem 6666  creur 6673  replimt 6692  reim0bt 6712  absnidt 6798  absort 6800  seq1bnd 6847  seq1ublem 6848  cau5i 6854  cau4i 6855  cau5 6856  cvg3 6860  facdivt 6879  facndivt 6880  facwordit 6881  faclbnd 6882  faclbnd6 6891  bccl2t 6909  climcl 6916  fsum1 6943  fsumcllem 6952  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  csbfsumlem 6964  fsumcom 6966  fsumrev 6967  fsumshftm 6970  fsummulc1 6971  fsummulc2 6972  fsum2mul 6975  fsumconst 6976  fsumcmp 6978  fsumabs 6981  serzrelem 6999  binomlem6 7009  bcxmas 7014  clm3 7017  clm4 7018  climconst 7031  climconst2 7032  2climnn 7039  2climnn0 7040  climrecl 7047  climge0 7049  climaddlem3 7052  climaddc1 7054  climaddc2 7055  climmullem5 7060  climmullem8 7063  climsubc2 7067  clim2serzt 7070  climcmplem 7073  climcmpc1 7075  climsqueeze 7076  climsqueeze2 7077  climsup 7091  climcau 7092  caucvglem4 7096  caucvglem6 7098  caucvg3lem 7102  serzf0 7105  ser1f0 7106  ser1const 7107  ser1cmp 7110  ser1cmp2 7113  cvgcmp3c 7122  isumclim2tf 7133  isum1p 7141  isumreclt 7145  isummulc1 7147  isummulc1ALT 7148  isumcmpi 7150  reccnv 7153  expcnvlem6 7167  expcnv 7168  geoser 7169  georeclim 7175  cvgratlem1ALT 7182  cvgratlem2ALT 7183  cvgratlem3ALT 7184  cvgratlem1 7185  cvgratlem2 7186  cvgratlem3 7187  cvgratlem4 7188  fsum0diaglem2 7192  fsum0diag2 7194  fsum0diag3 7195  fsum0diag4 7196  elcncf 7200  cncffvelrnOLD 7202  cncffvelrn 7203  mulc1cncf 7214  ivthlem1 7216  ivthlem7 7222  ivthlem9 7224  ivthlem7OLD 7231  efseq1ex 7248  efseq0ex 7253  efaddlem16 7295  efaddlem27 7306  efne0t 7311  efexpt 7314  eftlclt 7321  abspef01tlub 7336  reeff1o 7368  sin01bndlem2 7410  cos01bndlem2 7412  cos01gt0 7419  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  acdcALT 7438  znnen 7445  unbenlem 7447  infpnlem1 7449  infxpidmlem1 7495  infxpidmlem7 7501  infxpidmlem8 7502  infxpidmlem10 7504  infxpidmlem11 7505  infxpidmlem12 7506  infcda 7510  infdif 7511  infdif2 7512  infxp 7515  alephadd 7524  uniopnt 7540  istps2 7549  bastgt 7564  tgclt 7566  tgval3t 7567  tgtopt 7570  bastopt 7575  tgss2t 7579  subbas 7586  subtop 7588  indistop 7590  iincld 7621  clsval2 7627  iscld3 7637  isopn3 7639  0ntr 7644  elcls3 7652  neiint 7660  neii1 7662  neii2 7663  0nnei 7667  neips 7668  opnneissb 7669  opnssneib 7670  neindisj 7672  tpnei 7675  unnei 7676  innei 7677  opnneiid 7678  neissex 7679  islp2 7688  clslp 7689  cnpimaex 7704  cnpco 7708  cnsscnp 7711  cncnplem4 7716  cncnp 7717  cncnp2 7718  cnconst 7719  hausnei 7723  sncld 7726  dnsconst 7727  metxp 7774  bl2in 7783  rnblssm 7791  blss 7793  blssex 7794  ssbl 7795  opni2 7805  blssopn 7807  opnuni 7808  opnin 7809  opntop 7810  unirnbl 7815  blopn 7816  metcnp 7826  metcn 7828  metcnpi3 7831  metcnpi4 7832  metcni2 7834  metcnss 7837  metdnsconst 7840  cncfmet 7844  tgioolem 7853  tgioo 7854  dscmet 7856  lmconst 7872  lmuni 7886  lmsslem 7887  lmfexlem3 7893  lmle 7895  metelcls 7900  metcnp4lem2 7903  metcnp4 7904  metcn4i 7906  xpcn 7910  bopcn 7919  fsumcnlem 7923  iscms2lem4 7926  iscms2lem5 7927  iscms2 7928  iscms2i 7929  lmcau 7930  cmsss 7931  bcthlem2 7934  bcthlem8 7940  bcthlem10 7942  bcthlem13 7945  bcthlem14 7946  bcthlem16 7948  bcthlem17 7949  bcthlem18 7950  bcthlem20 7952  bcthlem31 7963  isgrp 7975  grpidinvlem3 7984  grpideu 7987  grplcan 8010  grpinvf 8014  grpnnncan2 8028  grplactf1o 8034  subgopr 8055  subgabl 8060  ring2 8086  nvex 8169  isnvi 8171  isnviOLD 8172  nvmf 8206  nvmul0or 8212  nvz 8236  nvcni 8266  nmcnilem 8272  sm1cnilem 8281  sspg 8321  ssps 8323  sspmlem 8325  sspmval 8326  nmoub3i 8368  0lno 8382  nmlno0lem 8385  nmlnoubi 8388  ipsubdir 8439  sspph 8446  ubthlem2 8461  ubthlem4 8463  ubthlem5 8464  ubthlem6 8465  ubthlem10 8469  ubthlem11 8470  minveceu 8514  htthlem7 8556  htthlem12 8561  pilem1 8590  efifolem2 8638  efifolem5 8641  efifolem6 8642  efif1lem5 8649  eff1i 8665  hvmul0ort 8815  hiidge0t 8885  his6t 8886  hial0 8889  hial02 8890  normgt0tOLD 8914  normgt0t 8915  normpyct 8934  shsubcltOLD 9011  hlimcaui 9027  chsscm 9033  chcmh 9034  ocsh 9072  occont 9076  ocorth 9080  occllem6 9094  projlem16 9117  projlem21 9122  projlem25 9126  projlem28 9129  projlem31 9132  pjtheu 9150  shsel3t 9194  shsel1t 9200  shmods 9277  chssoct 9334  h1de2b 9392  h1de2bOLD 9393  h1de2ctlem 9394  spansneleq 9409  spansneleqOLD 9410  spansnss2t 9415  spanpr 9420  h1datom 9421  cm2jt 9480  osumlem5 9499  osumlem7 9501  spansnm0 9512  spansncv 9514  pjvect 9558  pjocvect 9559  pjjs 9562  pjsumt 9572  hon0 9636  hoaddsubt 9659  eigorth 9680  nmopub2tALT 9750  unopf1ot 9756  cnvunopt 9758  unoplint 9760  counopt 9761  nmfnleub2t 9766  hmopadj2t 9781  hmoplint 9782  bralnfnt 9788  nmlnop0ALT 9835  lnopeq0 9847  nmopunt 9854  hmopst 9860  hmopmt 9861  hmopcot 9863  nmcopexlem1 9866  nmcopexlem6 9871  nmophm 9876  lnopcon 9878  lnopcnbdt 9880  nmcfnexlem1 9895  nmcfnexlem6 9900  lnfncon 9905  lnfncnbdt 9907  nlelch 9909  riesz3 9910  riesz1t 9913  cnlnadjlem2 9916  cnlnssadj 9928  nmopadjlem 9937  adjmult 9939  adjaddt 9940  nmoptri 9941  nmopco 9942  nmopcoadj 9948  branmfnt 9951  rnbra 9953  kbass6t 9966  leopaddt 9977  leopmulit 9978  leopmul2it 9980  pjnmop 9986  hmopidmchlem 9989  pjnormss 10007  stclt 10053  hst1ht 10064  hstlest 10068  stge1 10075  stle 10077  stadd 10083  stadd3 10085  strlem1 10087  stcltrlem1 10113  cvcon3t 10121  cvnbtwnt 10123  mdbr3 10134  mdbr4 10135  dmdmdt 10137  dmdbr3 10141  dmdbr4 10142  mdsl0 10145  mdsl2b 10158  mdslmd1lem1 10160  mdslmd1lem2 10161  mdslmd1 10164  mdslmd3 10167  csmdsym 10169  mdexch 10170  atsseq 10182  atom1d 10188  superpos 10189  hatomistic 10197  cvbr3 10202  atcv0eq 10214  atcv1t 10215  atexcht 10216  atoml 10217  atoml2 10218  atord 10219  atcvatlem 10220  atcvat 10221  atcvat2 10222  irredlem1 10225  irredlem4 10228  irred 10229  atcvat3 10231  atcvat4 10232  atabs 10236  mdsymlem4 10241  mdsymlem5 10242  mdsymlem6 10243  sumdmdi 10249  sumdmdlem 10252  dmdbr5at 10255  cdjreu 10264  cdj1 10265  cdj3lem1 10266  cdj3lem2b 10269  cdj3 10273  lemul2itALT 10275  ghomcl 10297  ghomid 10299  ghomf1olem 10301  rcla4devOLD 10331  uninqs 10342  infi1 10347  fine 10348  abfi 10349  ficli 10368  f2imacnv 10370  oooeqim2 10371  fiv 10374  fiiu2 10377  clsrebb 10380  cdrci 10381  truni1 10386  esnnei 10395  mapdiscn 10398  cmphmp 10408  cnvhmpha 10412  hmphsyma 10415  hmeogrp 10425  homcard 10426  qusp 10430  filint 10437  fipfil 10438  fipfil2 10439  oefil2 10441  fgsb 10444  efilcp 10445  infi 10448  fgsb2 10449  efilcp2 10450  cnfilca 10451  iintlem1 10476  iint 10478  trnij 10481  rdmob 10525  rcmob 10526  cmpmorp 10556  ehm 10563  dehm 10564  cehm 10565  mrdmcd 10566  cmpassoh 10573  homgrf 10574  imonclem 10583  ismonc 10584  cmpmon 10585  icmpmon 10587  idmon 10588  fmamo 10594  vidfunid 10595  iddvvidd 10596  idcvvidc 10597
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain