Theorem ex 114

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.) (Contributed by NM, 5-Aug-1993.) (Proof 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		ax-ia3 107	. 2 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
2		exp.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl6 33	1 |- ( ph -> ( ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  expcom  115  bi3  118  expd  256  impancom  258  expimpd  358  exp31  359  exp32  360  exp4b  362  exp41  365  exp43  367  exp53  372  impr  374  simplbi2  380  anidms  392  syl2anc  406  pm5.74da  437  imdistanda  442  pm5.32da  445  a2and  530  impbida  568  anim12dan  572  pm2.01da  608  pm2.65da  633  mtand  637  pm5.21im  668  jao  727  jaoian  767  jaodan  769  dcim  809  stdcn  815  impidc  826  pm2.5gdc  834  con1bidc  842  con2bidc  843  con1bdc  846  pm5.18dc  851  dfandc  852  pm4.63dc  854  pm4.54dc  870  pm5.21nd  884  dcan  901  dcor  902  annimdc  904  pm4.55dc  905  pm3.11dc  924  pm3.12dc  925  prlem1  940  pm3.2an3  1143  3jcad  1145  3impia  1161  3an1rs  1180  3exp1  1184  3exp2  1186  exp520  1189  syl3anl2  1248  3jaoian  1266  3jaodan  1267  mp3anl1  1292  mp3anl2  1293  mp3anl3  1294  inegd  1333  xor3dc  1348  pm5.15dc  1350  xor2dc  1351  xornbidc  1352  xordc  1353  nbbndc  1355  biassdc  1356  dfbi3dc  1358  pm5.24dc  1359  alanimi  1418  equsexd  1690  sbequ1  1724  sbiedv  1745  ax11v2  1774  equs5or  1784  sbequi  1793  exlimdd  1826  exlimddv  1852  cbvaldva  1878  cbvexdva  1879  nfsbxyt  1894  sbcomxyyz  1921  nfsb4t  1965  eupickbi  2057  moexexdc  2059  euexex  2060  2euswapdc  2066  dvelimdc  2275  nebidc  2362  rgen2a  2460  ralimiaa  2468  ralimdaa  2472  ralrimiva  2479  ralrimdva  2486  ralrimivva  2488  ralrimdvv  2490  ralrimdvva  2491  reximdva  2508  reximssdv  2510  reximddv2  2511  rexlimiva  2518  rexlimdva  2523  rexlimdvva  2531  r19.29vva  2551  2gencl  2690  vtocldf  2708  spcimdv  2741  spcimedv  2743  rspct  2753  eqvinc  2778  eqvincg  2779  ceqex  2782  reu6  2842  eqreu  2845  sbciedf  2912  rmob  2969  csbiebt  3005  csbiedf  3006  eqelssd  3082  reupick  3326  reximdva0m  3344  ssn0  3371  rgenm  3431  eqifdc  3472  preqr1g  3659  prel12  3664  dfnfc2  3720  intssunim  3759  intab  3766  iineq2d  3799  ssiun2  3822  mpteq2da  3977  exmid01  4081  pwntru  4082  exmid1dc  4083  exmidn0m  4084  exmidsssnc  4086  exmidundif  4089  exmidundifim  4090  copsexg  4126  copsex2t  4127  sess1  4219  sess2  4220  frirrg  4232  tron  4264  onelss  4269  onintss  4272  abnexg  4327  reusv1  4339  reusv3  4341  rabxfrd  4350  iunpw  4361  ssorduni  4363  ordsson  4368  ordsucg  4378  onintrab2im  4394  onsucelsucexmidlem  4404  elirr  4416  en2lp  4429  ordsuc  4438  ordpwsucss  4442  ordtri2or2exmid  4446  reg3exmidlemwe  4453  tfisi  4461  omsinds  4495  nnpredcl  4496  sosng  4572  2optocl  4576  relop  4649  releldmb  4736  relelrnb  4737  elrnmptg  4751  elreimasng  4863  relbrcnvg  4876  trin2  4888  ssxpbm  4932  ssxp1  4933  ssxp2  4934  elxp4  4984  elxp5  4985  relresfld  5026  relcoi1  5028  iotaval  5057  iotass  5063  funmo  5096  imadif  5161  imain  5163  2elresin  5192  feu  5263  fcnvres  5264  f0rn0  5275  f1oun  5343  f1oprg  5365  relfvssunirn  5391  funbrfv  5414  funbrfv2b  5420  dffn5im  5421  dfimafn  5424  funimass4  5426  ssimaex  5436  fvmptssdm  5459  fvmptf  5467  elfvmptrab1  5469  fvimacnv  5489  funimass3  5490  elpreima  5493  elrnrexdm  5513  eldmrexrn  5515  dffo4  5522  dffo5  5523  fmpt  5524  fmptdf  5531  ffvresb  5537  resflem  5538  fmptco  5540  fsn  5546  funfvima  5603  funfvima2  5604  f1mpt  5626  f1imass  5629  f1ocnvfvrneq  5637  foeqcnvco  5645  f1eqcocnv  5646  fliftfun  5651  fliftf  5654  isopolem  5677  isosolem  5679  eusvobj2  5714  acexmidlemab  5722  oprabid  5757  ovidi  5843  ovg  5863  suppssfv  5932  suppssov1  5933  funrnex  5966  f1dmex  5968  oprabexd  5979  fo2ndresm  6014  oprssdmm  6023  op1steq  6031  dfoprab3  6043  fo2ndf  6078  f1o2ndf1  6079  poxp  6083  spc2ed  6084  f1od2  6086  rbropapd  6093  reldmtpos  6104  rntpos  6108  tposf2  6119  tposf12  6120  issmo2  6140  smores  6143  smoiso  6153  tfrlem9  6170  tfrlemibacc  6177  tfrlemibfn  6179  tfrlemi14d  6184  tfrexlem  6185  tfr1onlembacc  6193  tfr1onlembfn  6195  tfr1onlemres  6200  tfri1dALT  6202  tfrcllembacc  6206  tfrcllembfn  6208  tfrcllemres  6213  tfrcl  6215  rdgivallem  6232  frecabcl  6250  frecrdg  6259  oawordi  6319  nnmcom  6339  nnsucelsuc  6341  nntri3or  6343  nnsucuniel  6345  nntri1  6346  nnsseleq  6351  nntr2  6353  dcdifsnid  6354  nnaordi  6358  nnmord  6367  nnaordex  6377  nnm00  6379  ertr  6398  erex  6407  iserd  6409  iinerm  6455  erinxp  6457  qsel  6460  qliftfun  6465  qliftfund  6466  2ecoptocl  6471  brecop  6473  mapss  6539  ixpssmap2g  6575  ixpssmapg  6576  dom2lem  6620  fundmen  6654  unen  6664  enm  6667  xpdom2  6678  fopwdom  6683  xpf1o  6691  mapen  6693  mapxpen  6695  ssenen  6698  phplem4  6702  nneneq  6704  snnen2og  6706  phplem4dom  6709  nndomo  6711  phpm  6712  phplem4on  6714  fidifsnen  6717  dif1enen  6727  fin0  6732  fin0or  6733  findcard2  6736  findcard2s  6737  findcard2d  6738  findcard2sd  6739  ac6sfi  6745  fimax2gtri  6748  finexdc  6749  en2eqpr  6754  onunsnss  6758  unfidisj  6763  undifdcss  6764  undifdc  6765  fiintim  6770  xpfi  6771  fisseneq  6773  ssfirab  6774  fnfi  6777  iunfidisj  6786  f1finf1o  6787  en1eqsnbi  6789  fidcenum  6796  isbth  6807  ssfii  6814  fieq0  6816  eqsupti  6835  suplub2ti  6840  isotilem  6845  supisoex  6848  eqinfti  6859  inflbti  6863  ordiso2  6872  djulclb  6892  updjudhf  6916  updjud  6919  difinfsn  6937  difinfinf  6938  ctmlemr  6945  ctm  6946  ctssdclemn0  6947  ctssdccl  6948  ctssdc  6950  enumct  6952  enomnilem  6960  finomni  6962  exmidomniim  6963  exmidomni  6964  fodjuomnilemdc  6966  fodjuomnilemres  6970  nnnninf  6973  ismkvnex  6979  mkvprop  6982  fodjumkvlemres  6983  pm54.43  6996  pr2nelem  6997  pr2ne  6998  exmidfodomrlemim  7005  exmidfodomrlemr  7006  exmidfodomrlemrALT  7007  acfun  7011  ccfunen  7027  mulcanpig  7091  nlt1pig  7097  addcmpblnq  7123  ltsonq  7154  ltexnqq  7164  prarloclemarch2  7175  enq0tr  7190  addcmpblnq0  7199  addnq0mo  7203  mulnq0mo  7204  prcdnql  7240  prcunqu  7241  prarloclemlo  7250  prarloclem3step  7252  prarloclem3  7253  genpdflem  7263  genpelvl  7268  genpelvu  7269  genpcdl  7275  genpcuu  7276  genprndl  7277  genprndu  7278  genpdisj  7279  addnqprllem  7283  addnqprulem  7284  addlocprlemeq  7289  addlocprlemgt  7290  nqprloc  7301  nqprl  7307  nqpru  7308  addnqprlemrl  7313  addnqprlemru  7314  addnqprlemfl  7315  addnqprlemfu  7316  prmuloc  7322  prmuloc2  7323  mullocpr  7327  mulnqprlemrl  7329  mulnqprlemru  7330  mulnqprlemfl  7331  mulnqprlemfu  7332  distrlem4prl  7340  distrlem4pru  7341  ltprordil  7345  1idprl  7346  1idpru  7347  ltpopr  7351  ltsopr  7352  ltaddpr  7353  ltexprlemm  7356  ltexprlemlol  7358  ltexprlemupu  7360  ltexprlemdisj  7362  ltexprlemloc  7363  ltexprlemrl  7366  ltexprlemru  7368  addcanprleml  7370  addcanprlemu  7371  addcanprg  7372  ltaprg  7375  recexprlemlol  7382  recexprlemdisj  7386  recexprlemloc  7387  recexprlem1ssl  7389  recexprlem1ssu  7390  aptiprleml  7395  aptiprlemu  7396  ltmprr  7398  archpr  7399  cauappcvgprlemm  7401  cauappcvgprlemopl  7402  cauappcvgprlemlol  7403  cauappcvgprlemopu  7404  cauappcvgprlemrnd  7406  cauappcvgprlemloc  7408  cauappcvgprlemladdfu  7410  cauappcvgprlemladdfl  7411  cauappcvgprlemladdru  7412  cauappcvgprlemladdrl  7413  caucvgprlemnkj  7422  caucvgprlemm  7424  caucvgprlemopl  7425  caucvgprlemlol  7426  caucvgprlemopu  7427  caucvgprlemrnd  7429  caucvgprlemloc  7431  caucvgprlemladdfu  7433  caucvgprlemladdrl  7434  caucvgprlemlim  7437  caucvgprprlemnkltj  7445  caucvgprprlemnkeqj  7446  caucvgprprlemnjltk  7447  caucvgprprlemml  7450  caucvgprprlemopl  7453  caucvgprprlemlol  7454  caucvgprprlemopu  7455  caucvgprprlemrnd  7457  caucvgprprlemloc  7459  caucvgprprlemexbt  7462  caucvgprprlemexb  7463  caucvgprprlemlim  7467  mulcmpblnrlemg  7483  addsrmo  7486  mulsrmo  7487  ltsrprg  7490  srpospr  7525  caucvgsrlemgt1  7537  cnm  7567  pitonn  7583  nntopi  7629  axcaucvglemcau  7633  axcaucvglemres  7634  lelttr  7775  ltletr  7776  readdcan  7825  cnegexlem1  7860  cnegexlem2  7861  addid0  8054  lelttrdi  8107  add20  8155  eqord1  8164  recexre  8258  inelr  8264  rimul  8265  apreap  8267  ltmul1  8272  cru  8282  apreim  8283  apirr  8285  apsym  8286  apcotr  8287  apadd1  8288  apneg  8291  mulext1  8292  msqge0  8296  mulge0  8299  apti  8302  ltleap  8311  recexap  8327  mulap0b  8329  mul0eqap  8344  recgt0  8518  prodgt02  8521  prodge02  8523  lemul12b  8529  lemul12a  8530  nnrecgt0  8668  addltmul  8860  nominpos  8861  elnnz  8968  peano2z  8994  zaddcllempos  8995  zaddcl  8998  zletric  9002  zlelttric  9003  zltnle  9004  zleloe  9005  zrevaddcl  9008  nzadd  9010  zdceq  9030  zdcle  9031  zdclt  9032  nn0n0n1ge2b  9034  nn0lt2  9036  zextle  9046  peano5uzti  9063  uzind2  9067  fzind  9070  fnn0ind  9071  nn0ind-raph  9072  btwnz  9074  eluzuzle  9236  uz11  9250  eluzp1m1  9251  supinfneg  9292  infsupneg  9293  lbzbi  9310  qapne  9333  qreccl  9336  qrevaddcl  9338  irradd  9340  irrmul  9341  ledivge1le  9412  nn0ledivnn  9447  xrlelttr  9482  xrltletr  9483  npnflt  9491  nmnfgt  9494  xnn0lenn0nn0  9541  xnn0xadd0  9543  xleadd1  9551  xle2add  9555  xposdif  9558  xlesubadd  9559  ixxss1  9580  ixxss2  9581  ixxss12  9582  iccid  9601  elioc2  9612  elico2  9613  elicc2  9614  fznlem  9714  fzn  9715  fzen  9716  0fz1  9718  uzsubsubfz  9720  fzopth  9734  fzss1  9736  fzss2  9737  elfz1b  9763  uzsplit  9765  fzm1  9773  fznuz  9775  fzrevral  9778  elfz0ubfz0  9795  elfz0fzfz0  9796  fz0fzelfz0  9797  difelfzle  9804  1fv  9809  fzoss1  9841  fzosplit  9847  fzouzsplit  9849  fzonmapblen  9857  fzofzim  9858  eluzgtdifelfzo  9867  elfzodifsumelfzo  9871  elfzom1p1elfzo  9884  ssfzo12  9894  ssfzo12bi  9895  fzofzp1b  9898  elfzonelfzo  9900  subfzo0  9912  qtri3or  9913  qletric  9914  qlelttric  9915  qltnle  9916  qdceq  9917  exbtwnzlemstep  9918  exbtwnzlemshrink  9919  exbtwnzlemex  9920  exbtwnz  9921  rebtwn2zlemstep  9923  rebtwn2z  9925  ioom  9931  ico0  9932  ioc0  9933  flltdivnn0lt  9970  flqeqceilz  9984  modqid2  10017  modqmuladd  10032  modqmuladdim  10033  modqmuladdnn0  10034  modqm1p1mod0  10041  modaddmodlo  10054  modfzo0difsn  10061  addmodlteq  10064  frec2uzuzd  10068  frec2uzltd  10069  frec2uzlt2d  10070  frec2uzrand  10071  frec2uzf1od  10072  frec2uzrdg  10075  frecuzrdgtcl  10078  frecuzrdgdomlem  10083  frecuzrdgfunlem  10085  frecfzennn  10092  uzennn  10102  uzsinds  10108  seq3clss  10133  iseqf1olemqf1o  10159  seq3f1olemp  10168  seq3id3  10173  seq3id  10174  seq3z  10177  ser3ge0  10183  expcl2lemap  10198  leexp2r  10240  leexp1a  10241  zesq  10303  expnbnd  10308  nn0opthlem2d  10360  nn0opthd  10361  facdiv  10377  facndiv  10378  facwordi  10379  faclbnd  10380  faclbnd6  10383  facubnd  10384  bcval4  10391  bcpasc  10405  bccl  10406  fiinfnf1o  10425  fihashf1rn  10428  hashunlem  10443  fiprsshashgt1  10456  hashfzo  10461  hashfzp1  10463  hashxp  10465  hashfacen  10472  zfz1iso  10477  seq3coll  10478  ovshftex  10484  reim0b  10527  cjap  10571  caucvgrelemcau  10644  caucvgre  10645  cvg1nlemres  10649  r19.29uz  10656  r19.2uz  10657  recvguniq  10659  sqrt0  10668  resqrexlemover  10674  resqrexlemdecn  10676  resqrexlemlo  10677  resqrexlemcalc3  10680  resqrexlemglsq  10686  resqrexlemga  10687  rsqrmo  10691  sqrtsq  10708  abs00ap  10726  absnid  10737  qabsor  10739  absexpzap  10744  abs3lem  10775  cau3lem  10778  caubnd2  10781  icodiamlt  10844  maxleim  10869  maxabslemlub  10871  maxabslemval  10872  fimaxre2  10890  negfi  10891  minmax  10893  xrmaxleim  10905  xrmaxiflemlub  10909  xrmaxiflemval  10911  xrminmax  10926  clim  10942  climuni  10954  climcn1  10969  climcn2  10970  mulcn2  10973  iserex  11000  climcau  11008  climcaucn  11012  sumrbdclem  11037  fsum3cvg  11038  summodclem2a  11042  zsumdc  11045  fsum3  11048  isumz  11050  fsumf1o  11051  fisumss  11053  fsum3cvg3  11057  fsumsplit  11068  fsum2dlemstep  11095  fsumconst  11115  modfsummod  11119  fsum00  11123  fsumabs  11126  fsumrelem  11132  fsumiun  11138  bcxmas  11150  isumsplit  11152  divcnv  11158  cvgratnnlemnexp  11185  cvgratnnlemmn  11186  mertenslem2  11197  efexp  11239  efieq1re  11328  eirrap  11332  dvdsval2  11344  moddvds  11350  dvds0  11356  absdvdsb  11359  dvdsabsb  11360  dvdsmul1  11363  dvdscmul  11368  dvdsmulc  11369  dvds2ln  11374  dvds2add  11375  dvds2sub  11376  dvdslelemd  11389  dvdsleabs2  11392  dvds1  11399  dvdsext  11401  fzo0dvdseq  11403  dvdsfac  11406  mulmoddvds  11409  odd2np1  11418  oddge22np1  11426  evennn02n  11427  evennn2n  11428  mulsucdiv2z  11430  sqoddm1div8z  11431  ltoddhalfle  11438  halfleoddlt  11439  m1expo  11445  nn0ehalf  11448  nn0o  11452  nn0oddm1d2  11454  nnoddm1d2  11455  divalglemeunn  11466  divalglemex  11467  divalglemeuneg  11468  flodddiv4  11479  zsupcllemstep  11486  dvdsbnd  11493  dvdslegcd  11501  gcdeq0  11513  gcd0id  11515  gcdneg  11518  gcdaddm  11520  gcdabs  11524  bezoutlemnewy  11530  bezoutlemstep  11531  bezoutlemzz  11536  bezoutlemaz  11537  bezoutlembz  11538  bezoutlembi  11539  bezoutlemeu  11541  bezoutlemle  11542  bezoutlemsup  11543  dvdsgcd  11546  dfgcd2  11548  rppwr  11562  dvdssqlem  11564  bezoutr1  11567  algfx  11579  eucalglt  11584  eucalgcvga  11585  lcmledvds  11597  lcmeq0  11598  lcmneg  11601  lcmabs  11603  lcmgcdlem  11604  lcmdvds  11606  lcmgcdeq  11610  coprmgcdb  11615  ncoprmgcdne1b  11616  coprmdvds  11619  qredeq  11623  qredeu  11624  rpdvds  11626  divgcdcoprm0  11628  divgcdcoprmex  11629  cncongr1  11630  cncongr2  11631  isprm2lem  11643  prmind2  11647  dvdsnprmd  11652  divgcdodd  11667  coprm  11668  isprm6  11671  prmfac1  11676  rpexp  11677  sqrt2irr  11686  pw2dvdseu  11691  sqrt2irrap  11703  nonsq  11730  hashdvds  11742  phimullem  11746  ennnfonelemk  11758  ennnfoneleminc  11769  ennnfonelemkh  11770  ennnfonelemhf1o  11771  ennnfonelemhom  11773  ennnfonelemrnh  11774  ennnfonelemdm  11778  ennnfone  11783  exmidunben  11784  ctinfom  11786  ctinf  11788  unct  11797  uniopn  12011  toponcomb  12038  bastg  12073  tgcl  12076  tgdom  12084  en1top  12089  tgss3  12090  bastop2  12096  epttop  12102  iuncld  12127  isopn3  12137  neiint  12157  neisspw  12160  0nnei  12165  neipsm  12166  opnneissb  12167  opnssneib  12168  tpnei  12172  neiuni  12173  opnneiid  12176  neissex  12177  ssrest  12194  tgcn  12219  tgcnp  12220  iscnp4  12229  cnpnei  12230  cnntr  12236  cnss1  12237  cnss2  12238  cncnp2m  12242  cnrest2  12247  cnrest2r  12248  cnptopresti  12249  cnptoprest2  12251  cndis  12252  lmss  12257  txcnp  12282  upxp  12283  txcn  12286  txdis1cn  12289  txlm  12290  xblss2ps  12393  xblss2  12394  xblm  12406  blin2  12421  blbas  12422  xmeter  12425  isxms2  12441  metss  12483  metrest  12495  xmettxlem  12498  xmettx  12499  fsumcncntop  12542  rescncf  12554  cncfss  12556  cncfco  12564  cncfmptc  12568  mulcncflem  12576  mulcncf  12577  expcncf  12578  limcdifap  12587  limcimo  12590  cnplimcim  12592  cnplimccntop  12595  limccnp2lem  12601  dvfgg  12612  dvcnp2cntop  12618  cbvrald  12687  uzdcinzz  12697  bdsepnft  12777  peano5set  12830  findset  12835  bj-omtrans  12846  bj-findis  12869  strcollnft  12874  pwtrufal  12884  exmid1stab  12887  subctctexmid  12888  peano4nninf  12892  nninfalllem1  12895  nninfall  12896  nninfsellemqall  12903  nninfomnilem  12906  nninffeq  12908  exmidsbthrlem  12909  exmidsbth  12911  sbthom  12913  isomninnlem  12917  trilpolemlt1  12926