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 476  pm2.61dan 477  condan 478  anabss7 503  impbida 518  3imtr3g 551  pm5.74da 585  ibib 589  jcad 599  pm5.32da 648  pm5.21nd 679  mpan 694  mpan2 695  mpdan 703  mpanl1 705  mpanl2 706  mpanr1 708  mpanr2 709  mpanlr1 710  nbn2 720  ecase3 751  ecase 752  3adantl1 802  3adantl2 803  3adantl3 804  3jcad 819  3impia 829  3an1rs 844  3exp1 848  3exp2 850  syl3anl1 872  syl3anl2 873  syl3anl3 874  3jaoian 888  3jaodan 889  mp3anl1 909  mp3anl2 910  mp3anl3 911  19.21ad 1058  equs4 1149  dvelimfALT 1152  a4imed 1160  sbequ1 1178  ax11v2 1215  sbequi 1228  hbsb4 1248  dvelimdf 1251  sbcom 1258  sbcom2 1334  sbal1 1346  dvelimALT 1353  ax11indi 1367  ax11inda 1371  a12stdy4 1375  a12lem1 1376  a12study 1378  a12studyALT 1379  euor2 1437  moexex 1438  rgen2a 1698  r19.20ia 1704  r19.20da 1707  r19.21aiva 1713  r19.21adva 1718  r19.21advv 1720  r19.21advva 1721  r19.22dva 1738  r19.23aiva 1743  r19.23adva 1746  2gencl 1827  vtocl2ga 1851  vtocl3ga 1852  rcla4edv 1877  ceqex 1884  reu3 1929  sspss 2143  sspsstr 2149  psssstr 2150  neldif 2163  reuss2 2273  reupick 2277  ssne0 2303  disjne 2313  pssdifn0 2327  sspr 2473  prel12 2482  intssuni 2552  ssiun2 2590  opabsb 2812  pwssun 2824  sotrieq 2858  reuuni2f 2880  ralxfrd 2894  iunpw 2911  efrirr 2925  dfwe2 2932  wefrc 2940  ordelord 2967  tz7.7 2970  ordsseleq 2973  onfr 2983  ordon 2984  ssorduni 2990  ordtr2 2999  ordunidif 3002  onint 3003  onint0 3004  onintss 3008  oninton 3009  onnminsb 3013  oneqmini 3014  oneqmin 3015  onminex 3017  ordsssuc2 3056  onmindif2 3058  ordsuc 3062  ordpwsuc 3063  ordsucelsuc 3070  ordtri2or2 3075  ordsucun 3079  onsucuni2 3088  nlimsucg 3109  unizlim 3110  ordunisuc2 3112  limsuc 3117  limsssuc 3118  tfi 3123  dfom2 3130  limomss 3134  limom 3143  peano5 3150  nn0suc 3151  findsg 3154  tfinds 3158  tfindsg 3159  tfindsg2 3160  2optocl 3233  relop 3272  relimasn 3422  dffun7 3537  imadif 3571  2elresin 3595  funrnex 3610  zfrep6 3611  fnopabg 3612  fcoi1 3642  fcoi2 3643  feu 3644  fcnvres 3645  f1oun 3703  f1dmex 3707  funbrfv 3747  fnopabfv 3755  dfimafn 3758  funimass4 3760  ssimaex 3765  funfv 3767  fvco 3771  fvco2 3772  fvopabn 3783  eqfnfv 3794  fvimacnv 3802  funimass3 3803  dff2 3814  dffo4 3817  dffo5 3818  fopab2 3820  fopabco 3829  fsn 3831  fconst5 3845  funfvima 3849  funfvima2 3850  funiunfv 3863  isotr 3894  isotrALT 3895  isomin 3896  isofrlem 3898  tfrlem1 3908  tfrlem5 3912  tfrlem9 3916  tfrlem11 3918  rdgsucopabn 3944  rdglim2 3946  tz7.48-2 3954  tz7.48-3 3955  abianfplem 3958  abianfp 3959  ndmoprcl 4041  oe0lem 4149  oevn0 4151  omcl 4168  oecl 4169  oa0r 4170  om1r 4174  oe1m 4176  oaordi 4177  oawordex 4188  oaordex 4189  oaass 4192  omordi 4194  omord 4196  omcan 4197  omwordi 4199  om00 4203  omlimcl 4206  odi 4207  omass 4208  oneo 4209  oen0 4210  oeordi 4211  oecan 4213  oewordi 4215  oewordri 4216  oeworde 4217  oeordsuc 4218  oelim2 4219  nnmcom 4238  nnmordi 4243  oaabs 4249  nneob 4252  erthi 4278  erdisj 4283  2ecoptocl 4301  brecop 4303  th3qlem1 4311  breng 4370  brdomg 4371  dom2d 4398  ensymg 4405  fundmen 4422  undom 4431  xpdom2 4435  pw2en 4439  sbthlem1 4440  sdomnsym 4455  sdomdomtr 4462  ensdomtr 4464  domsdomtr 4469  enen1 4470  enen2 4471  domen1 4472  domen2 4473  sdomen1 4474  fodomr 4476  2pwuninel 4480  mapenlem2 4483  mapen 4484  mapdom2 4487  mapunen 4495  ssenen 4497  phplem4 4504  nneneq 4505  php 4506  php3 4508  onomeneq 4511  nndomo 4513  pssinf 4520  pssnn 4526  ssfi 4528  unblem2 4531  unblem3 4532  isfinite2 4536  unfi 4541  fiint 4547  fodomfi 4553  fodomfib 4554  iunfi 4556  pm54.43 4559  supnub 4569  supmaxlem 4575  suppr 4577  supsnALT 4579  suc11reg 4592  inf3lem1 4600  inf3lem5 4604  inf3lem6 4605  infensuc 4625  noinfep 4627  trcl 4632  zfregs 4634  r1tr 4641  r1ord 4642  r1val1 4645  ssrankr1 4663  r1pwcl 4674  rankonid 4682  rankxplim 4699  rankxplim3 4701  hta 4715  aceq5lem4 4725  aceq5 4727  aceq6b 4729  ac5b 4740  ac6lem 4741  kmlem11 4762  zorn2lem4 4778  zorn2lem6 4780  zorn2lem7 4781  fodomb 4787  brdom6disj 4792  unidom 4795  uniimadom 4797  carddomi 4822  sucdom 4829  sdomsdomcard 4835  cardlim 4838  ondomcard 4844  carduni 4845  cardiun 4846  cardmin 4847  alephon 4852  alephcard 4854  alephnbtwn 4855  alephordi 4861  alephord2i 4864  alephsucdom 4867  cardaleph 4872  cardalephex 4873  cardinfima 4878  alephval2 4889  alephval3 4890  cfub 4895  cflim 4896  axextnd 4930  axrepndlem1 4931  axrepndlem2 4932  axunnd 4935  axpowndlem2 4937  axpowndlem3 4938  axpowndlem4 4939  axpownd 4940  axregndlem2 4942  axregnd 4943  axinfndlem1 4944  axinfnd 4945  axacndlem4 4949  axacndlem5 4950  axacnd 4951  mulcanpi 5014  nlt1pi 5020  indpi 5021  ordpipq 5043  ltexpq 5067  prcdpq 5084  genpnnp 5095  genpcd 5096  1pr 5104  distrlem4pr 5117  distrlem5pr 5118  1idpr 5120  prlem934 5126  ltexprlem2 5130  ltexprlem3 5131  ltexprlem4 5132  ltexprlem7 5135  ltexpri 5136  addcanpr 5139  prlem936b 5141  prlem936 5142  reclem2pr 5144  reclem3pr 5145  reclem4pr 5146  suplem1pr 5148  suplem2pr 5149  ltsrpr 5173  suppsr2 5210  suppsr3 5211  supsrlem2 5213  supsr 5218  cnegextlem1 5332  cnegextlem2 5333  cnegextlem3 5334  negeu 5342  addsubt 5371  1re 5422  0re 5427  letrt 5512  xrlttrit 5539  xrletrt 5551  addgegt0 5588  recext 5671  mulcan2t 5676  receu 5684  div23t 5719  div13t 5720  div12t 5721  divadddivt 5754  prodge0 5790  prodgt02t 5797  prodge02t 5799  ltmul2 5804  lemul1 5805  lemul2 5806  lemul1it 5807  lemul1itOLD 5808  lemul12ait 5812  lemul12itOLD 5813  lemul12it 5814  mulgt1t 5815  lediv1t 5820  ltmuldiv2t 5832  ltdivmult 5833  ledivmult 5834  lemuldiv2t 5839  ltdiv2t 5849  ledivp1 5868  ltdivp1 5869  nnrecgt0t 5914  nominpos 6004  lbreu 6006  sup2 6012  suprleub 6020  infmsup 6029  infmrcl 6030  xrsupexmnf 6035  xrinfmexpnf 6036  xrsupsslem 6037  xrinfmsslem 6038  xrub 6041  supxrre 6044  supxrpnf 6049  supxrunb1 6050  supxrunb2 6051  supxrbnd 6052  supxrleub 6060  lt0nnn0 6077  nn0ge0t 6078  nnnn0addclt 6086  elnnz 6106  nn0subt 6122  zaddclt 6126  zrevaddclt 6131  elnn0nn 6132  zltp1let 6142  zextlet 6150  btwnnzt 6153  peano2uz2 6163  uzind2 6168  uzindOLD 6170  uzwo4OLD 6172  uzwo5OLD 6173  nn0ind-raph 6176  btwnz 6177  uzwo3lem1 6178  zmax 6182  zbtwnre 6183  flval3t 6200  qrecclt 6228  qrevaddclt 6230  qbtwnre 6233  qsqueeze 6235  monoord 6249  seq1lem1 6264  seq1rn2 6276  seq1res 6282  ser1add2 6293  ser1add 6294  seq1shftid 6311  iooval2t 6322  elioo4g 6336  elioc2t 6340  elico2t 6341  elicc2t 6342  uzss 6381  uz11t 6382  eluzp1m1t 6383  uzwo 6405  uzwoOLD 6406  fznt 6443  fzoptht 6452  elfzp1 6460  fzrevralt 6469  fsequb 6473  seqzfveq 6504  seqzrn2 6506  ser0cl1 6514  expp1t 6524  expne0it 6538  expge0t 6541  expgt1t 6542  expwordit 6553  expword2it 6555  expmwordit 6556  exple1t 6557  sqlecant 6591  sq01t 6601  discrlem3 6608  nn0opthlem2 6615  nn0opthlem2OLD 6616  sqr0 6623  sqrlem12 6635  sqr11 6654  sqr2irr 6680  inelr 6686  crulem 6687  creur 6694  replimt 6713  reim0bt 6734  reim0btOLD 6735  absnidt 6825  absort 6827  seq1bnd 6876  seq1ublem 6877  cau5i 6883  cau4i 6884  cau5 6885  cvg3 6889  facdivt 6908  facndivt 6909  facwordit 6910  faclbnd 6911  faclbnd6 6920  bccl2t 6939  climcl 6946  fsum1 6973  fsumcllem 6982  fsum1ps 6986  fsumsplit 6988  fsumadd 6990  csbfsumlem 6994  fsumcom 6996  fsumrev 6997  fsumshftm 7000  fsummulc1 7001  fsummulc2 7002  fsum2mul 7005  fsumconst 7006  fsumcmp 7008  fsumabs 7011  serzrelem 7029  binomlem6 7039  bcxmas 7044  clm3 7047  clm4 7048  climconst 7062  climconst2 7063  2climnn 7070  2climnn0 7071  climrecl 7078  climge0 7080  climaddlem3 7085  climaddc1 7087  climaddc2 7088  climmullem5 7093  climmullem8 7096  climsubc2 7100  clim2serzt 7103  climcmplem 7106  climcmpc1 7108  climsqueeze 7109  climsqueeze2 7110  climsup 7124  climcau 7125  caucvglem4 7129  caucvglem6 7131  caucvg3lem 7136  caucvg3lemOLD 7137  serzf0 7140  ser1f0 7141  ser1const 7142  ser1cmp 7145  ser1cmp2 7148  cvgcmp3c 7157  isumclim2tf 7169  isum1p 7177  isumreclt 7181  isummulc1 7183  isummulc1ALT 7184  isumcmpi 7186  reccnv 7189  expcnvlem6 7203  expcnv 7204  geoser 7205  georeclim 7211  cvgratlem1ALT 7218  cvgratlem2ALT 7219  cvgratlem3ALT 7220  cvgratlem1 7221  cvgratlem2 7222  cvgratlem3 7223  cvgratlem4 7224  fsum0diaglem2 7228  fsum0diag2 7230  fsum0diag3 7231  fsum0diag4 7232  elcncf 7236  cncffvelrnOLD 7238  cncffvelrn 7239  mulc1cncf 7250  ivthlem1 7252  ivthlem7 7258  ivthlem9 7260  ivthlem7OLD 7267  efseq1ex 7284  efseq0ex 7289  efaddlem16 7331  efaddlem27 7342  efne0t 7347  efexpt 7350  eftlclt 7357  abspef01tlub 7372  reeff1o 7404  sin01bndlem2 7446  cos01bndlem2 7448  cos01gt0 7455  acdc3lem 7464  acdc2lem2 7467  acdc5lem2 7470  acdclem 7472  acdcALT 7474  znnen 7481  unbenlem 7483  infpnlem1 7485  infxpidmlem1 7531  infxpidmlem7 7537  infxpidmlem8 7538  infxpidmlem10 7540  infxpidmlem11 7541  infxpidmlem12 7542  infcda 7546  infdif 7547  infdif2 7548  infxp 7551  infpss 7553  alephadd 7561  uniopnt 7577  istps2 7586  bastgt 7601  tgclt 7603  tgval3t 7604  tgtopt 7607  bastopt 7612  tgss2t 7616  subbas 7623  subtop 7625  indistop 7627  iincld 7658  clsval2 7664  iscld3 7674  isopn3 7676  0ntr 7681  elcls3 7690  neiint 7698  neii1 7700  neii2 7701  0nnei 7705  neips 7706  opnneissb 7707  opnssneib 7708  neindisj 7710  tpnei 7713  unnei 7714  innei 7715  opnneiid 7716  neissex 7717  islp2 7726  clslp 7727  cnpimaex 7744  cnpco 7748  cnsscnp 7751  cncnplem4 7756  cncnp 7757  cncnp2 7758  cnconst 7759  hausnei 7763  sncld 7766  dnsconst 7767  metxp 7815  bl2in 7825  rnblssm 7833  blss 7835  blssOLD 7836  blssex 7837  ssbl 7838  opni2 7848  blssopn 7850  opnuni 7851  opnin 7852  opntop 7853  unirnbl 7858  blopn 7859  metcnp 7870  metcn 7872  metcnpi3 7875  metcnpi4 7876  metcni2 7878  metcnss 7881  metdnsconst 7884  cncfmet 7888  tgioolem 7897  tgioo 7898  dscmet 7901  lmconst 7917  lmuni 7934  lmsslem 7935  lmfexlem3 7941  lmle 7943  metelcls 7948  metcnp4lem2 7952  metcnp4 7953  metcn4i 7955  xpcn 7959  bopcn 7968  fsumcnlem 7972  iscms2lem4 7975  iscms2lem5 7976  iscms2 7977  iscms2i 7978  lmcau 7979  cmsss 7980  bcthlem2 7983  bcthlem8 7989  bcthlem10 7991  bcthlem13 7994  bcthlem14 7995  bcthlem16 7997  bcthlem17 7998  bcthlem18 7999  bcthlem20 8001  bcthlem31 8012  isgrp 8024  grpidinvlem3 8033  grpideu 8036  grplcan 8058  grpinvf 8062  grpnnncan2 8076  grplactf1o 8082  subgopr 8103  subgabl 8108  ring2 8134  nvex 8215  isnvi 8217  nvmf 8251  nvmul0or 8257  nvz 8282  nvcni 8315  nvcni2 8316  nvcni3 8317  nmcnilem 8323  sm1cnilem 8333  sspg 8373  ssps 8375  sspmlem 8377  sspmval 8378  nmoub3i 8421  0lno 8435  nmlno0lem 8438  nmlnoubi 8441  ipsubdir 8492  sspph 8499  ubthlem2 8514  ubthlem4 8516  ubthlem5 8517  ubthlem6 8518  ubthlem10 8522  ubthlem11 8523  minveceu 8567  htthlem7 8609  htthlem12 8614  spwpr3 8645  spwpr4 8646  spwpr4a 8647  pilem1 8654  efifolem2 8702  efifolem5 8705  efifolem6 8706  efif1lem5 8713  eff1i 8728  hvmul0ort 8878  hiidge0t 8948  his6t 8949  hial0 8952  hial02 8953  normgt0tOLD 8977  normgt0t 8978  normpyct 8997  shsubcltOLD 9078  hlimcaui 9094  chsscm 9100  chcmh 9101  ocsh 9144  occont 9148  ocorth 9152  occllem6 9166  projlem16 9189  projlem21 9194  projlem25 9198  projlem28 9201  projlem31 9204  pjtheu 9223  shsel3t 9267  shsel1t 9273  shmods 9350  chssoct 9407  h1de2b 9465  h1de2bOLD 9466  h1de2ctlem 9467  spansneleq 9482  spansneleqOLD 9483  spansnss2t 9488  spanpr 9493  h1datom 9494  cm2jt 9553  osumlem5 9572  osumlem7 9574  spansnm0 9585  spansncv 9587  spansncvOLD 9588  pjvect 9632  pjocvect 9633  pjjs 9636  pjsumt 9646  hon0 9710  hoaddsubt 9733  eigorth 9754  nmopub2tALT 9824  unopf1ot 9831  cnvunopt 9833  unoplint 9835  counopt 9836  nmfnleub2t 9841  hmopadj2t 9856  hmoplint 9857  bralnfnt 9863  nmlnop0ALT 9911  lnopeq0 9923  nmopunt 9930  hmopst 9936  hmopmt 9937  hmopcot 9939  nmcopexlem1 9942  nmcopexlem6 9947  nmophm 9952  lnopcon 9954  lnopcnbdt 9956  nmcfnexlem1 9971  nmcfnexlem6 9976  lnfncon 9981  lnfncnbdt 9983  nlelch 9985  riesz3 9986  riesz1t 9989  cnlnadjlem2 9992  cnlnssadj 10004  nmopadjlem 10013  adjmult 10016  adjaddt 10017  nmoptri 10018  nmopco 10019  nmopcoadj 10025  branmfnt 10029  rnbra 10031  kbass6t 10045  leopaddt 10056  leopmulit 10057  leopmul2it 10059  pjnmop 10066  hmopidmchlem 10069  pjnormss 10087  stclt 10134  hst1ht 10145  hstlest 10149  stge1 10156  stle 10158  stadd 10164  stadd3 10166  strlem1 10168  stcltrlem1 10194  cvcon3t 10202  cvnbtwnt 10204  mdbr3 10215  mdbr4 10216  dmdmdt 10218  dmdbr3 10223  dmdbr4 10224  dmdbr5 10226  mdsl0 10228  mdsl2b 10241  mdslmd1lem1 10243  mdslmd1lem2 10244  mdslmd1 10247  mdslmd3 10250  csmdsym 10252  mdexch 10253  atsseq 10265  atom1d 10271  superpos 10272  hatomistic 10280  cvbr3 10285  atcv0eq 10297  atcv1t 10298  atexcht 10299  atoml 10300  atoml2 10301  atord 10302  atcvatlem 10303  atcvat 10304  atcvat2 10305  irredlem1 10308  irredlem4 10311  irred 10312  atcvat3 10314  atcvat4 10315  atabs 10319  mdsymlem4 10324  mdsymlem5 10325  mdsymlem6 10326  sumdmdi 10333  sumdmdlem 10336  dmdbr5at 10340  cdjreu 10350  cdj1 10351  cdj3lem1 10352  cdj3lem2b 10355  cdj3 10359  lemul2itALT 10361  ghomcl 10383  ghomid 10385  ghomf1olem 10387  gelcomplOLD 10410  ee7.2a 10418  rcla4devOLD 10424  uninqs 10435  infi1 10440  fine 10441  abfi 10442  ficli 10461  f2imacnv 10463  oooeqim2 10464  fiv 10468  fiiu2 10471  clsrebb 10474  cdrci 10475  truni1 10480  esnnei 10489  mapdiscn 10492  cmphmp 10502  cnvhmpha 10506  hmphsyma 10509  hmeogrp 10519  homcard 10520  qusp 10524  filint 10531  fipfil 10532  fipfil2 10533  oefil2 10535  fgsb 10538  efilcp 10539  infi 10542  fgsb2 10543  efilcp2 10544  cnfilca 10545  rcfpfillem2 10547  rcfpfillem4 10549  rcfpfillem6 10551  iintlem1 10583  iint 10585  trnij 10588  rdmob 10632  rcmob 10633  cmpmorp 10663  ehm 10670  dehm 10671  cehm 10672  mrdmcd 10673  cmpassoh 10680  homgrf 10681  imonclem 10690  ismonc 10691  cmpmon 10692  icmpmon 10694  idmon 10695  fmamo 10701  vidfunid 10702  iddvvidd 10703  idcvvidc 10704  idfisf 10705

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