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

Step	Hyp	Ref	Expression
1		exp.1	. 2 |- ((ph /\ ps) -> ch)
2		impexp 347	. 2 |- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))
3	1, 2	mpbi 189	1 |- (ph -> (ps -> ch))

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 677  mpan 692  mpan2 693  mpdan 701  mpanl1 703  mpanl2 704  mpanr1 706  mpanr2 707  mpanlr1 708  nbn2 718  ecase3 749  ecase 750  3adantl1 800  3adantl2 801  3adantl3 802  3jcad 817  3impia 827  3an1rs 842  3exp1 846  3exp2 848  syl3anl1 869  syl3anl2 870  syl3anl3 871  3jaoian 885  3jaodan 886  mp3anl1 906  mp3anl2 907  mp3anl3 908  19.21ad 1035  equs4 1133  dvelimfALT 1136  a4c1 1144  sbequ1 1161  ax11v2 1199  sbequi 1212  hbsb4 1232  dvelimdf 1235  sbcom 1242  sbcom2 1316  sbal1 1328  ax11indi 1344  ax11inda 1348  a12stdy4 1352  a12lem1 1353  a12study 1355  a12studyALT 1356  euor2 1414  moexex 1415  rgen2a 1675  r19.20ia 1681  r19.20da 1684  r19.21aiva 1690  r19.21adva 1695  r19.21advv 1697  r19.21advva 1698  r19.22dva 1715  r19.23aiva 1720  r19.23adva 1723  2gencl 1804  vtocl2ga 1828  vtocl3ga 1829  ceqex 1858  reu3 1902  sspss 2116  sspsstr 2122  psssstr 2123  neldif 2136  reuss2 2246  reupick 2250  ssne0 2276  disjne 2286  pssdifn0 2300  sspr 2445  prel12 2454  intssuni 2523  ssiun2 2561  opabsb 2777  pwssun 2789  sotrieq 2825  reuuni2f 2846  ralxfrd 2860  iunpw 2877  efrirr 2891  dfwe2 2898  wefrc 2906  ordelord 2933  tz7.7 2936  ordsseleq 2939  onfr 2949  ordon 2950  ssorduni 2956  ordtr2 2965  ordunidif 2968  onint 2969  onint0 2970  onintss 2974  oninton 2975  onnminsb 2979  oneqmini 2980  oneqmin 2981  onminex 2983  ordsssuc2 3022  onmindif2 3024  ordsuc 3028  ordpwsuc 3029  ordsucelsuc 3036  ordtri2or2 3041  ordsucun 3045  onsucuni2 3054  nlimsucg 3075  unizlim 3076  ordunisuc2 3078  limsuc 3083  limsssuc 3084  tfi 3089  dfom2 3096  limomss 3100  limom 3109  peano5 3116  nn0suc 3117  findsg 3120  tfinds 3124  tfindsg 3125  tfindsg2 3126  2optocl 3198  relimasn 3376  relfld 3457  dffun7 3481  imadif 3514  2elresin 3538  funrnex 3553  zfrep6 3554  fnopabg 3555  fcoi1 3584  fcoi2 3585  feu 3586  fcnvres 3587  f1oun 3645  f1dmex 3649  funbrfv 3689  fnopabfv 3697  dfimafn 3700  funimass4 3702  ssimaex 3707  funfv 3709  fvco 3713  fvco2 3714  fvopabn 3725  eqfnfv 3736  fvimacnv 3744  funimass3 3745  dff2 3756  dffo4 3759  dffo5 3760  fopab2 3762  fopabco 3771  fsn 3773  fconst5 3787  funfvima 3791  funfvima2 3792  funiunfv 3805  isotr 3836  isotrALT 3837  isomin 3838  isofrlem 3840  tfrlem1 3850  tfrlem5 3854  tfrlem9 3858  tfrlem11 3860  rdgsucopabn 3886  rdglim2 3888  tz7.48-2 3896  tz7.48-3 3897  abianfplem 3900  abianfp 3901  ndmoprcl 3984  oe0lem 4090  oevn0 4092  omcl 4109  oecl 4110  oa0r 4111  om1r 4115  oe1m 4117  oaordi 4118  oawordex 4129  oaordex 4130  oaass 4133  omordi 4135  omord 4137  omcan 4138  omwordi 4140  om00 4144  omlimcl 4147  odi 4148  omass 4149  oneo 4150  oen0 4151  oeordi 4152  oecan 4154  oewordi 4156  oewordri 4157  oeworde 4158  oeordsuc 4159  oelim2 4160  nnmcom 4179  nnmordi 4184  oaabs 4190  nneob 4193  erthi 4219  erdisj 4224  2ecoptocl 4242  brecop 4244  th3qlem1 4252  breng 4311  brdomg 4312  dom2d 4339  ensymg 4346  fundmen 4363  undom 4372  xpdom2 4376  pw2en 4380  sbthlem1 4381  sdomnsym 4396  sdomdomtr 4403  ensdomtr 4405  domsdomtr 4410  enen1 4411  enen2 4412  domen1 4413  domen2 4414  sdomen1 4415  fodomr 4417  mapenlem2 4422  mapen 4423  mapdom2 4426  mapunen 4434  ssenen 4436  phplem4 4443  nneneq 4444  php 4445  php3 4447  onomeneq 4450  nndomo 4452  pssinf 4459  pssnn 4465  ssfi 4467  unblem2 4470  unblem3 4471  isfinite2 4475  unfi 4480  fiint 4486  fodomfi 4492  fodomfib 4493  iunfi 4495  pm54.43 4498  supnub 4508  suppr 4514  supsnALT 4516  suc11reg 4529  inf3lem1 4537  inf3lem5 4541  inf3lem6 4542  infensuc 4562  noinfep 4564  trcl 4569  zfregs 4571  r1tr 4578  r1ord 4579  r1val1 4582  ssrankr1 4600  r1pwcl 4611  rankonid 4619  rankxplim 4636  rankxplim3 4638  hta 4652  aceq5lem4 4662  aceq5 4664  aceq6b 4666  ac5b 4677  ac6lem 4678  kmlem11 4699  zorn2lem4 4715  zorn2lem6 4717  zorn2lem7 4718  fodomb 4724  brdom6disj 4729  unidom 4732  uniimadom 4734  carddomi 4758  sucdom 4765  sdomsdomcard 4771  cardlim 4774  ondomcard 4780  carduni 4781  cardiun 4782  cardmin 4783  alephon 4788  alephcard 4790  alephnbtwn 4791  alephordi 4797  alephord2i 4800  alephsucdom 4803  cardaleph 4808  cardalephex 4809  cardinfima 4814  alephval2 4825  alephval3 4826  cfub 4831  cflim 4832  axextnd 4866  axrepndlem1 4867  axrepndlem2 4868  axunnd 4871  axpowndlem2 4873  axpowndlem3 4874  axpowndlem4 4875  axpownd 4876  axregndlem2 4878  axregnd 4879  axinfndlem1 4880  axinfnd 4881  axacndlem4 4885  axacndlem5 4886  axacnd 4887  mulcanpi 4950  nlt1pi 4956  indpi 4957  ordpipq 4979  ltexpq 5003  prcdpq 5020  genpnnp 5031  genpcd 5032  1pr 5040  distrlem4pr 5053  distrlem5pr 5054  1idpr 5056  prlem934 5062  ltexprlem2 5066  ltexprlem3 5067  ltexprlem4 5068  ltexprlem7 5071  ltexpri 5072  addcanpr 5075  prlem936b 5077  prlem936 5078  reclem2pr 5080  reclem3pr 5081  reclem4pr 5082  suplem1pr 5084  suplem2pr 5085  ltsrpr 5109  suppsr2 5146  suppsr3 5147  supsrlem2 5149  supsr 5154  cnegextlem1 5268  cnegextlem2 5269  cnegextlem3 5270  negeu 5278  addsubt 5307  1re 5358  0re 5363  letrt 5449  xrlttrit 5476  xrletrt 5488  addgegt0 5525  recext 5608  mulcan2t 5613  receu 5621  div23t 5656  div13t 5657  div12t 5658  divadddivt 5691  prodge0 5727  prodgt02t 5734  prodge02t 5736  ltmul2 5741  lemul1 5742  lemul2 5743  lemul1it 5744  lemul1itOLD 5745  lemul12ait 5749  lemul12itOLD 5750  lemul12it 5751  mulgt1t 5752  lediv1t 5757  ltmuldiv2t 5769  ltdivmult 5770  ledivmult 5771  lemuldiv2t 5776  ltdiv2t 5786  ledivp1 5805  ltdivp1 5806  nnrecgt0t 5851  nominpos 5941  lbreu 5943  sup2 5949  suprleub 5957  infmsup 5966  infmrcl 5967  xrsupexmnf 5972  xrinfmexpnf 5973  xrsupsslem 5974  xrinfmsslem 5975  xrub 5978  supxrre 5981  supxrpnf 5986  supxrunb1 5987  supxrunb2 5988  supxrbnd 5989  supxrleub 5997  lt0nnn0 6014  nn0ge0t 6015  nnnn0addclt 6023  elnnz 6043  nn0subt 6059  zaddclt 6063  zrevaddclt 6068  elnn0nn 6069  zltp1let 6079  zextlet 6087  btwnnzt 6090  peano2uz2 6100  uzind2 6105  uzindOLD 6107  uzwo4OLD 6109  uzwo5OLD 6110  nn0ind-raph 6113  btwnz 6114  uzwo3lem1 6115  zmax 6119  zbtwnre 6120  flval3t 6133  qrecclt 6162  qrevaddclt 6164  qbtwnre 6167  qsqueeze 6169  monoord 6182  seq1lem1 6197  seq1rn2 6209  seq1res 6215  ser1add2 6226  ser1add 6227  seq1shftid 6244  iooval2t 6255  elioo4g 6269  elioc2t 6273  elico2t 6274  elicc2t 6275  uzss 6314  uz11t 6315  eluzp1m1t 6316  uzwo 6338  uzwoOLD 6339  fznt 6376  fzoptht 6385  elfzp1 6393  fzrevralt 6402  fsequb 6406  seqzfveq 6437  seqzrn2 6439  ser0cl1 6447  expp1t 6457  expne0it 6470  expge0t 6473  expgt1t 6474  expwordit 6485  expword2it 6487  expmwordit 6488  exple1t 6489  sqlecant 6523  sq01t 6533  discrlem3 6539  nn0opthlem2 6546  sqr0 6553  sqrlem12 6565  sqr11 6584  sqr2irr 6610  inelr 6616  crulem 6617  creur 6624  replimt 6643  reim0bt 6663  absnidt 6749  absort 6751  seq1bnd 6798  seq1ublem 6799  cau5i 6805  cau4i 6806  cau5 6807  cvg3 6811  facdivt 6830  facndivt 6831  facwordit 6832  faclbnd 6833  faclbnd6 6842  bccl2t 6860  climcl 6867  fsum1 6894  fsumcllem 6903  fsum1ps 6907  fsumsplit 6909  fsumadd 6911  csbfsumlem 6915  fsumcom 6917  fsumrev 6918  fsumshftm 6921  fsummulc1 6922  fsummulc2 6923  fsum2mul 6926  fsumconst 6927  fsumcmp 6929  fsumabs 6932  serzrelem 6950  binomlem6 6960  bcxmas 6965  clm3 6968  clm4 6969  climconst 6982  climconst2 6983  2climnn 6990  2climnn0 6991  climrecl 6998  climge0 7000  climaddlem3 7003  climaddc1 7005  climaddc2 7006  climmullem5 7011  climmullem8 7014  climsubc2 7018  clim2serzt 7021  climcmplem 7024  climcmpc1 7026  climsqueeze 7027  climsqueeze2 7028  climsup 7042  climcau 7043  caucvglem4 7047  caucvglem6 7049  caucvg3lem 7053  serzf0 7056  ser1f0 7057  ser1const 7058  ser1cmp 7061  ser1cmp2 7064  cvgcmp3c 7073  isumclim2tf 7084  isum1p 7092  isumreclt 7096  isummulc1 7098  isummulc1ALT 7099  isumcmpi 7101  reccnv 7104  expcnvlem6 7118  expcnv 7119  geoser 7120  georeclim 7126  cvgratlem1ALT 7133  cvgratlem2ALT 7134  cvgratlem3ALT 7135  cvgratlem1 7136  cvgratlem2 7137  cvgratlem3 7138  cvgratlem4 7139  fsum0diaglem2 7143  fsum0diag2 7145  fsum0diag3 7146  fsum0diag4 7147  elcncf 7151  cncffvelrnOLD 7153  cncffvelrn 7154  mulc1cncf 7165  ivthlem1 7167  ivthlem7 7173  ivthlem9 7175  ivthlem7OLD 7182  efseq1ex 7199  efseq0ex 7204  efaddlem16 7246  efaddlem27 7257  efne0t 7262  efexpt 7265  eftlclt 7272  abspef01tlub 7287  reeff1o 7319  sin01bndlem2 7361  cos01bndlem2 7363  cos01gt0 7370  acdc3lem 7379  acdc2lem2 7382  acdc5lem2 7385  acdclem 7387  acdcALT 7389  znnen 7396  unbenlem 7398  infpnlem1 7400  infxpidmlem1 7446  infxpidmlem7 7452  infxpidmlem8 7453  infxpidmlem10 7455  infxpidmlem11 7456  infxpidmlem12 7457  infcda 7461  infdif 7462  infdif2 7463  infxp 7466  alephadd 7475  uniopnt 7491  istps2 7500  bastgt 7515  tgclt 7517  tgval3t 7518  tgtopt 7521  bastopt 7526  tgss2t 7530  subbas 7537  subtop 7539  indistop 7541  iincld 7572  clsval2 7578  iscld3 7588  isopn3 7590  0ntr 7594  elcls3 7600  neiint 7608  neii1 7610  neii2 7611  0nnei 7615  neips 7616  opnneissb 7617  opnssneib 7618  neindisj 7620  tpnei 7623  unnei 7624  innei 7625  opnneiid 7626  neissex 7627  islp2 7636  clslp 7637  cnpimaex 7652  cnpco 7656  cnsscnp 7659  cncnplem4 7664  cncnp 7665  cncnp2 7666  cnconst 7667  hausnei 7671  sncld 7674  dnsconst 7675  metxp 7722  bl2in 7731  rnblssm 7739  blss 7741  blssex 7742  ssbl 7743  opni2 7753  blssopn 7755  opnuni 7756  opnin 7757  opntop 7758  unirnbl 7763  blopn 7764  metcnp 7774  metcn 7776  metcnpi3 7779  metcnpi4 7780  metcni2 7782  metcnss 7785  metdnsconst 7788  cncfmet 7792  tgioolem 7801  tgioo 7802  dscmet 7804  lmconst 7820  lmuni 7834  lmsslem 7835  lmfexlem3 7841  lmle 7843  metelcls 7848  metcnp4lem2 7851  metcnp4 7852  metcn4i 7854  xpcn 7858  bopcn 7867  fsumcnlem 7871  iscms2lem4 7874  iscms2lem5 7875  iscms2 7876  iscms2i 7877  lmcau 7878  cmsss 7879  bcthlem2 7882  bcthlem8 7888  bcthlem10 7890  bcthlem13 7893  bcthlem14 7894  bcthlem16 7896  bcthlem17 7897  bcthlem18 7898  bcthlem20 7900  bcthlem31 7911  isgrp 7923  grpidinvlem3 7932  grpideu 7935  grplcan 7958  grpinvf 7962  grpnnncan2 7976  grplactf1o 7982  subgopr 8003  subgabl 8008  ring2 8034  isnvi 8110  nvmf 8143  nvmul0or 8149  nvz 8173  nvcni 8203  nmcnilem 8209  sm1cnilem 8216  sspg 8256  ssps 8258  sspmlem 8260  sspmval 8261  nmoub3i 8303  0lno 8317  nmlno0lem 8320  nmlnoubi 8323  ipsubdir 8374  sspph 8381  ubthlem2 8396  ubthlem4 8398  ubthlem5 8399  ubthlem6 8400  ubthlem10 8404  ubthlem11 8405  minveceu 8449  htthlem7 8490  htthlem12 8495  pilem1 8503  efifolem2 8551  efifolem5 8554  efifolem6 8555  efif1lem5 8562  eff1i 8578  lemul2itALT 8637  ghomcl 8659  ghomid 8661  ghomf1olem 8663  rcla4dev 8691  uninqs 8701  infi1 8706  fine 8707  abfi 8708  ficli 8727  fiv 8731  fiiu2 8734  clsrebb 8737  cdrci 8738  truni1 8743  esnnei 8750  cmphmp 8759  cnvhmpha 8763  hmphsyma 8766  hmeogrp 8776  qusp 8780  filint 8787  fipfil 8788  fipfil2 8789  oefil2 8791  fgsb 8794  efilcp 8795  infi 8798  fgsb2 8799  efilcp2 8800  cnfilca 8801  iintlem1 8826  iint 8828  trnij 8831  rdmob 8875  rcmob 8876  cmpmorp 8906  ehm 8913  dehm 8914  cehm 8915  mrdmcd 8916  cmpassoh 8923  homgrf 8924  imonclem 8933  ismonc 8934  cmpmon 8935  icmpmon 8937  fmamo 8942  vidfunid 8943  hvmul0ort 9043  hiidge0t 9113  his6t 9114  hial0 9117  hial02 9118  normgt0tOLD 9142  normgt0t 9143  normpyct 9162  shsubcltOLD 9241  hlimcaui 9257  chsscm 9263  chcmh 9264  ocsh 9286  occont 9290  ocorth 9294  occllem6 9308  projlem16 9331  projlem21 9336  projlem25 9340  projlem28 9343  projlem31 9346  pjtheu 9364  shsel3t 9408  shsel1t 9414  shmods 9491  chssoct 9548  h1de2b 9606  h1de2bOLD 9607  h1de2ctlem 9608  spansneleq 9623  spansneleqOLD 9624  spansnss2t 9629  spanpr 9634  h1datom 9635  cm2jt 9694  osumlem5 9713  osumlem7 9715  spansnm0 9726  spansncv 9728  pjvect 9772  pjocvect 9773  pjjs 9776  pjsumt 9786  hon0 9850  hoaddsubt 9873  eigorth 9894  nmopub2tALT 9964  unopf1ot 9970  cnvunopt 9972  unoplint 9974  counopt 9975  nmfnleub2t 9980  hmopadj2t 9995  hmoplint 9996  bralnfnt 10002  nmlnop0ALT 10049  lnopeq0 10061  nmopunt 10068  hmopst 10074  hmopmt 10075  hmopcot 10077  nmcopexlem1 10080  nmcopexlem6 10085  nmophm 10090  lnopcon 10092  lnopcnbdt 10094  nmcfnexlem1 10109  nmcfnexlem6 10114  lnfncon 10119  lnfncnbdt 10121  nlelch 10123  riesz3 10124  riesz1t 10127  cnlnadjlem2 10130  cnlnssadj 10142  nmopadjlem 10151  adjmult 10153  adjaddt 10154  nmoptri 10155  nmopco 10156  nmopcoadj 10162  branmfnt 10165  rnbra 10167  kbass6t 10180  leopaddt 10191  leopmulit 10192  leopmul2it 10194  pjnmop 10200  hmopidmchlem 10203  pjnormss 10221  stclt 10267  hst1ht 10278  hstlest 10282  stge1 10289  stle 10291  stadd 10297  stadd3 10299  strlem1 10301  stcltrlem1 10327  cvcon3t 10335  cvnbtwnt 10337  mdbr3 10348  mdbr4 10349  dmdmdt 10351  dmdbr3 10355  dmdbr4 10356  mdsl0 10359  mdsl2b 10372  mdslmd1lem1 10374  mdslmd1lem2 10375  mdslmd1 10378  mdslmd3 10381  csmdsym 10383  mdexch 10384  atsseq 10396  atom1d 10402  superpos 10403  hatomistic 10411  cvbr3 10416  atcv0eq 10428  atcv1t 10429  atexcht 10430  atoml 10431  atoml2 10432  atord 10433  atcvatlem 10434  atcvat 10435  atcvat2 10436  irredlem1 10439  irredlem4 10442  irred 10443  atcvat3 10445  atcvat4 10446  atabs 10450  mdsymlem4 10455  mdsymlem5 10456  mdsymlem6 10457  sumdmdi 10463  sumdmdlem 10466  dmdbr5at 10469  cdjreu 10478  cdj1 10479  cdj3lem1 10480  cdj3lem2b 10483  cdj3 10487

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