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-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  expcom  115  bi3  118  expd  256  impancom  258  expimpd  360  exp31  361  exp32  362  exp4b  364  exp41  367  exp43  369  exp53  374  impr  376  simplbi2  382  anidms  394  syl2anc  408  pm5.74da  439  imdistanda  444  pm5.32da  447  adantl4r  508  adantl5r  516  adantl6r  517  a2and  547  impbida  585  anim12dan  589  pm2.01da  625  pm2.65da  650  mtand  654  pm5.21im  685  jao  744  jaoian  784  jaodan  786  dcim  826  stdcn  832  impidc  843  pm2.5gdc  851  con1bidc  859  con2bidc  860  con1bdc  863  pm5.18dc  868  dfandc  869  pm4.63dc  871  pm4.54dc  887  pm5.21nd  901  dcan  918  dcor  919  annimdc  921  pm4.55dc  922  pm3.11dc  941  pm3.12dc  942  prlem1  957  pm3.2an3  1160  3jcad  1162  3impia  1178  3an1rs  1197  3exp1  1201  3exp2  1203  exp520  1206  syl3anl2  1265  3jaoian  1283  3jaodan  1284  mp3anl1  1309  mp3anl2  1310  mp3anl3  1311  inegd  1350  xor3dc  1365  pm5.15dc  1367  xor2dc  1368  xornbidc  1369  xordc  1370  nbbndc  1372  biassdc  1373  dfbi3dc  1375  pm5.24dc  1376  alanimi  1435  equsexd  1707  sbequ1  1741  sbiedv  1762  ax11v2  1792  equs5or  1802  sbequi  1811  exlimdd  1844  exlimddv  1870  cbvaldva  1900  cbvexdva  1901  nfsbxyt  1916  sbcomxyyz  1945  nfsb4t  1989  eupickbi  2081  moexexdc  2083  euexex  2084  2euswapdc  2090  dvelimdc  2301  nebidc  2388  rgen2a  2486  ralimiaa  2494  ralimdaa  2498  ralrimiva  2505  ralrimdva  2512  ralrimivva  2514  ralrimdvv  2516  ralrimdvva  2517  reximdva  2534  reximssdv  2536  reximddv2  2537  rexlimiva  2544  rexlimdva  2549  rexlimdvva  2557  r19.29vva  2577  2gencl  2719  vtocldf  2737  spcimdv  2770  spcimedv  2772  rspct  2782  eqvinc  2808  eqvincg  2809  ceqex  2812  reu6  2873  eqreu  2876  sbciedf  2944  rmob  3001  csbiebt  3039  csbiedf  3040  eqelssd  3116  reupick  3360  reximdva0m  3378  ssn0  3405  rgenm  3465  eqifdc  3506  preqr1g  3693  prel12  3698  dfnfc2  3754  intssunim  3793  intab  3800  iineq2d  3833  ssiun2  3856  mpteq2da  4017  exmid01  4121  pwntru  4122  exmid1dc  4123  exmidn0m  4124  exmidsssnc  4126  exmidundif  4129  exmidundifim  4130  copsexg  4166  copsex2t  4167  sess1  4259  sess2  4260  frirrg  4272  tron  4304  onelss  4309  onintss  4312  abnexg  4367  reusv1  4379  reusv3  4381  rabxfrd  4390  iunpw  4401  ssorduni  4403  ordsson  4408  ordsucg  4418  onintrab2im  4434  onsucelsucexmidlem  4444  elirr  4456  en2lp  4469  ordsuc  4478  ordpwsucss  4482  ordtri2or2exmid  4486  reg3exmidlemwe  4493  tfisi  4501  omsinds  4535  nnpredcl  4536  sosng  4612  2optocl  4616  relop  4689  releldmb  4776  relelrnb  4777  elrnmptg  4791  elreimasng  4905  relbrcnvg  4918  trin2  4930  ssxpbm  4974  ssxp1  4975  ssxp2  4976  elxp4  5026  elxp5  5027  relresfld  5068  relcoi1  5070  iotaval  5099  iotass  5105  funmo  5138  imadif  5203  imain  5205  2elresin  5234  feu  5305  fcnvres  5306  f0rn0  5317  f1oun  5387  f1oprg  5411  relfvssunirn  5437  funbrfv  5460  funbrfv2b  5466  dffn5im  5467  dfimafn  5470  funimass4  5472  ssimaex  5482  fvmptssdm  5505  fvmptf  5513  elfvmptrab1  5515  fvimacnv  5535  funimass3  5536  elpreima  5539  elrnrexdm  5559  eldmrexrn  5561  dffo4  5568  dffo5  5569  fmpt  5570  fmptdf  5577  ffvresb  5583  resflem  5584  fmptco  5586  fsn  5592  funfvima  5649  funfvima2  5650  f1mpt  5672  f1imass  5675  f1ocnvfvrneq  5683  foeqcnvco  5691  f1eqcocnv  5692  fliftfun  5697  fliftf  5700  isopolem  5723  isosolem  5725  eusvobj2  5760  acexmidlemab  5768  oprabid  5803  ovidi  5889  ovg  5909  suppssfv  5978  suppssov1  5979  funrnex  6012  f1dmex  6014  oprabexd  6025  fo2ndresm  6060  oprssdmm  6069  op1steq  6077  dfoprab3  6089  fo2ndf  6124  f1o2ndf1  6125  poxp  6129  spc2ed  6130  f1od2  6132  rbropapd  6139  reldmtpos  6150  rntpos  6154  tposf2  6165  tposf12  6166  issmo2  6186  smores  6189  smoiso  6199  tfrlem9  6216  tfrlemibacc  6223  tfrlemibfn  6225  tfrlemi14d  6230  tfrexlem  6231  tfr1onlembacc  6239  tfr1onlembfn  6241  tfr1onlemres  6246  tfri1dALT  6248  tfrcllembacc  6252  tfrcllembfn  6254  tfrcllemres  6259  tfrcl  6261  rdgivallem  6278  frecabcl  6296  frecrdg  6305  oawordi  6365  nnmcom  6385  nnsucelsuc  6387  nntri3or  6389  nnsucuniel  6391  nntri1  6392  nnsseleq  6397  nntr2  6399  dcdifsnid  6400  nnaordi  6404  nnmord  6413  nnaordex  6423  nnm00  6425  ertr  6444  erex  6453  iserd  6455  iinerm  6501  erinxp  6503  qsel  6506  qliftfun  6511  qliftfund  6512  2ecoptocl  6517  brecop  6519  mapss  6585  ixpssmap2g  6621  ixpssmapg  6622  dom2lem  6666  fundmen  6700  unen  6710  enm  6714  xpdom2  6725  fopwdom  6730  xpf1o  6738  mapen  6740  mapxpen  6742  ssenen  6745  phplem4  6749  nneneq  6751  snnen2og  6753  phplem4dom  6756  nndomo  6758  phpm  6759  phplem4on  6761  fidifsnen  6764  dif1enen  6774  fin0  6779  fin0or  6780  findcard2  6783  findcard2s  6784  findcard2d  6785  findcard2sd  6786  ac6sfi  6792  fimax2gtri  6795  finexdc  6796  en2eqpr  6801  onunsnss  6805  unfidisj  6810  undifdcss  6811  undifdc  6812  fiintim  6817  xpfi  6818  fisseneq  6820  ssfirab  6822  fnfi  6825  iunfidisj  6834  f1finf1o  6835  en1eqsnbi  6837  fidcenum  6844  isbth  6855  ssfii  6862  fieq0  6864  eqsupti  6883  suplub2ti  6888  isotilem  6893  supisoex  6896  eqinfti  6907  inflbti  6911  ordiso2  6920  djulclb  6940  updjudhf  6964  updjud  6967  difinfsn  6985  difinfinf  6986  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumct  7000  enomnilem  7010  finomni  7012  exmidomniim  7013  exmidomni  7014  fodjuomnilemdc  7016  fodjuomnilemres  7020  nnnninf  7023  ismkvnex  7029  mkvprop  7032  fodjumkvlemres  7033  pm54.43  7046  pr2nelem  7047  pr2ne  7048  exmidfodomrlemim  7057  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  acfun  7063  ccfunen  7079  mulcanpig  7143  nlt1pig  7149  addcmpblnq  7175  ltsonq  7206  ltexnqq  7216  prarloclemarch2  7227  enq0tr  7242  addcmpblnq0  7251  addnq0mo  7255  mulnq0mo  7256  prcdnql  7292  prcunqu  7293  prarloclemlo  7302  prarloclem3step  7304  prarloclem3  7305  genpdflem  7315  genpelvl  7320  genpelvu  7321  genpcdl  7327  genpcuu  7328  genprndl  7329  genprndu  7330  genpdisj  7331  addnqprllem  7335  addnqprulem  7336  addlocprlemeq  7341  addlocprlemgt  7342  nqprloc  7353  nqprl  7359  nqpru  7360  addnqprlemrl  7365  addnqprlemru  7366  addnqprlemfl  7367  addnqprlemfu  7368  prmuloc  7374  prmuloc2  7375  mullocpr  7379  mulnqprlemrl  7381  mulnqprlemru  7382  mulnqprlemfl  7383  mulnqprlemfu  7384  distrlem4prl  7392  distrlem4pru  7393  ltprordil  7397  1idprl  7398  1idpru  7399  ltpopr  7403  ltsopr  7404  ltaddpr  7405  ltexprlemm  7408  ltexprlemlol  7410  ltexprlemupu  7412  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemrl  7418  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  addcanprg  7424  ltaprg  7427  recexprlemlol  7434  recexprlemdisj  7438  recexprlemloc  7439  recexprlem1ssl  7441  recexprlem1ssu  7442  aptiprleml  7447  aptiprlemu  7448  ltmprr  7450  archpr  7451  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemopu  7456  cauappcvgprlemrnd  7458  cauappcvgprlemloc  7460  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemnkj  7474  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemopu  7479  caucvgprlemrnd  7481  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlemlim  7489  caucvgprprlemnkltj  7497  caucvgprprlemnkeqj  7498  caucvgprprlemnjltk  7499  caucvgprprlemml  7502  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemopu  7507  caucvgprprlemrnd  7509  caucvgprprlemloc  7511  caucvgprprlemexbt  7514  caucvgprprlemexb  7515  caucvgprprlemlim  7519  suplocexprlemrl  7525  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemloc  7529  suplocexprlemex  7530  suplocexprlemlub  7532  mulcmpblnrlemg  7548  addsrmo  7551  mulsrmo  7552  ltsrprg  7555  srpospr  7591  caucvgsrlemgt1  7603  map2psrprg  7613  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  cnm  7640  pitonn  7656  nntopi  7702  axcaucvglemcau  7706  axcaucvglemres  7707  axpre-suploclemres  7709  lelttr  7852  ltletr  7853  readdcan  7902  cnegexlem1  7937  cnegexlem2  7938  addid0  8135  lelttrdi  8188  add20  8236  eqord1  8245  recexre  8340  inelr  8346  rimul  8347  apreap  8349  ltmul1  8354  cru  8364  apreim  8365  apirr  8367  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  msqge0  8378  mulge0  8381  apti  8384  ltleap  8394  aprcl  8408  recexap  8414  mulap0b  8416  mul0eqap  8431  recgt0  8608  prodgt02  8611  prodge02  8613  lemul12b  8619  lemul12a  8620  nnrecgt0  8758  addltmul  8956  nominpos  8957  elnnz  9064  peano2z  9090  zaddcllempos  9091  zaddcl  9094  zletric  9098  zlelttric  9099  zltnle  9100  zleloe  9101  zrevaddcl  9104  nzadd  9106  zdceq  9126  zdcle  9127  zdclt  9128  nn0n0n1ge2b  9130  nn0lt2  9132  zextle  9142  peano5uzti  9159  uzind2  9163  fzind  9166  fnn0ind  9167  nn0ind-raph  9168  btwnz  9170  eluzuzle  9334  uz11  9348  eluzp1m1  9349  supinfneg  9390  infsupneg  9391  lbzbi  9408  qapne  9431  qreccl  9434  qrevaddcl  9436  irradd  9438  irrmul  9439  ledivge1le  9513  nn0ledivnn  9554  xrlelttr  9589  xrltletr  9590  npnflt  9598  nmnfgt  9601  xnn0lenn0nn0  9648  xnn0xadd0  9650  xleadd1  9658  xle2add  9662  xposdif  9665  xlesubadd  9666  ixxss1  9687  ixxss2  9688  ixxss12  9689  iccid  9708  elioc2  9719  elico2  9720  elicc2  9721  fznlem  9821  fzn  9822  fzen  9823  0fz1  9825  uzsubsubfz  9827  fzopth  9841  fzss1  9843  fzss2  9844  elfz1b  9870  uzsplit  9872  fzm1  9880  fznuz  9882  fzrevral  9885  elfz0ubfz0  9902  elfz0fzfz0  9903  fz0fzelfz0  9904  difelfzle  9911  1fv  9916  fzoss1  9948  fzosplit  9954  fzouzsplit  9956  fzonmapblen  9964  fzofzim  9965  eluzgtdifelfzo  9974  elfzodifsumelfzo  9978  elfzom1p1elfzo  9991  ssfzo12  10001  ssfzo12bi  10002  fzofzp1b  10005  elfzonelfzo  10007  subfzo0  10019  qtri3or  10020  qletric  10021  qlelttric  10022  qltnle  10023  qdceq  10024  exbtwnzlemstep  10025  exbtwnzlemshrink  10026  exbtwnzlemex  10027  exbtwnz  10028  rebtwn2zlemstep  10030  rebtwn2z  10032  ioom  10038  ico0  10039  ioc0  10040  flltdivnn0lt  10077  flqeqceilz  10091  modqid2  10124  modqmuladd  10139  modqmuladdim  10140  modqmuladdnn0  10141  modqm1p1mod0  10148  modaddmodlo  10161  modfzo0difsn  10168  addmodlteq  10171  frec2uzuzd  10175  frec2uzltd  10176  frec2uzlt2d  10177  frec2uzrand  10178  frec2uzf1od  10179  frec2uzrdg  10182  frecuzrdgtcl  10185  frecuzrdgdomlem  10190  frecuzrdgfunlem  10192  frecfzennn  10199  uzennn  10209  uzsinds  10215  seq3clss  10240  iseqf1olemqf1o  10266  seq3f1olemp  10275  seq3id3  10280  seq3id  10281  seq3z  10284  ser3ge0  10290  expcl2lemap  10305  leexp2r  10347  leexp1a  10348  zesq  10410  expnbnd  10415  nn0opthlem2d  10467  nn0opthd  10468  facdiv  10484  facndiv  10485  facwordi  10486  faclbnd  10487  faclbnd6  10490  facubnd  10491  bcval4  10498  bcpasc  10512  bccl  10513  fiinfnf1o  10532  fihashf1rn  10535  hashunlem  10550  fiprsshashgt1  10563  hashfzo  10568  hashfzp1  10570  hashxp  10572  hashfacen  10579  zfz1iso  10584  seq3coll  10585  ovshftex  10591  reim0b  10634  cjap  10678  caucvgrelemcau  10752  caucvgre  10753  cvg1nlemres  10757  r19.29uz  10764  r19.2uz  10765  recvguniq  10767  sqrt0  10776  resqrexlemover  10782  resqrexlemdecn  10784  resqrexlemlo  10785  resqrexlemcalc3  10788  resqrexlemglsq  10794  resqrexlemga  10795  rsqrmo  10799  sqrtsq  10816  abs00ap  10834  absnid  10845  qabsor  10847  absexpzap  10852  abs3lem  10883  cau3lem  10886  caubnd2  10889  icodiamlt  10952  maxleim  10977  maxabslemlub  10979  maxabslemval  10980  fimaxre2  10998  negfi  10999  minmax  11001  xrmaxleim  11013  xrmaxiflemlub  11017  xrmaxiflemval  11019  xrminmax  11034  clim  11050  climuni  11062  climcn1  11077  climcn2  11078  mulcn2  11081  iserex  11108  climcau  11116  climcaucn  11120  sumrbdclem  11146  fsum3cvg  11147  summodclem2a  11150  zsumdc  11153  fsum3  11156  isumz  11158  fsumf1o  11159  fisumss  11161  fsum3cvg3  11165  fsumsplit  11176  fsum2dlemstep  11203  fsumconst  11223  modfsummod  11227  fsum00  11231  fsumabs  11234  fsumrelem  11240  fsumiun  11246  bcxmas  11258  isumsplit  11260  divcnv  11266  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  mertenslem2  11305  ntrivcvgap  11317  prodrbdclem  11340  prodmodclem2a  11345  prodmodc  11347  efexp  11388  efieq1re  11478  eirrap  11484  dvdsval2  11496  moddvds  11502  dvds0  11508  absdvdsb  11511  dvdsabsb  11512  dvdsmul1  11515  dvdscmul  11520  dvdsmulc  11521  dvds2ln  11526  dvds2add  11527  dvds2sub  11528  dvdslelemd  11541  dvdsleabs2  11544  dvds1  11551  dvdsext  11553  fzo0dvdseq  11555  dvdsfac  11558  mulmoddvds  11561  odd2np1  11570  oddge22np1  11578  evennn02n  11579  evennn2n  11580  mulsucdiv2z  11582  sqoddm1div8z  11583  ltoddhalfle  11590  halfleoddlt  11591  m1expo  11597  nn0ehalf  11600  nn0o  11604  nn0oddm1d2  11606  nnoddm1d2  11607  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  flodddiv4  11631  zsupcllemstep  11638  dvdsbnd  11645  dvdslegcd  11653  gcdeq0  11665  gcd0id  11667  gcdneg  11670  gcdaddm  11672  gcdabs  11676  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemzz  11690  bezoutlemaz  11691  bezoutlembz  11692  bezoutlembi  11693  bezoutlemeu  11695  bezoutlemle  11696  bezoutlemsup  11697  dvdsgcd  11700  dfgcd2  11702  rppwr  11716  dvdssqlem  11718  bezoutr1  11721  algfx  11733  eucalglt  11738  eucalgcvga  11739  lcmledvds  11751  lcmeq0  11752  lcmneg  11755  lcmabs  11757  lcmgcdlem  11758  lcmdvds  11760  lcmgcdeq  11764  coprmgcdb  11769  ncoprmgcdne1b  11770  coprmdvds  11773  qredeq  11777  qredeu  11778  rpdvds  11780  divgcdcoprm0  11782  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  isprm2lem  11797  prmind2  11801  dvdsnprmd  11806  divgcdodd  11821  coprm  11822  isprm6  11825  prmfac1  11830  rpexp  11831  sqrt2irr  11840  pw2dvdseu  11846  sqrt2irrap  11858  nonsq  11885  hashdvds  11897  phimullem  11901  ennnfonelemk  11913  ennnfoneleminc  11924  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemhom  11928  ennnfonelemrnh  11929  ennnfonelemdm  11933  ennnfone  11938  exmidunben  11939  ctinfom  11941  ctinf  11943  enctlem  11945  unct  11954  uniopn  12168  toponcomb  12195  bastg  12230  tgcl  12233  tgdom  12241  en1top  12246  tgss3  12247  bastop2  12253  epttop  12259  iuncld  12284  isopn3  12294  neiint  12314  neisspw  12317  0nnei  12322  neipsm  12323  opnneissb  12324  opnssneib  12325  tpnei  12329  neiuni  12330  opnneiid  12333  neissex  12334  ssrest  12351  tgcn  12377  tgcnp  12378  iscnp4  12387  cnpnei  12388  cnntr  12394  cnss1  12395  cnss2  12396  cncnp2m  12400  cnrest2  12405  cnrest2r  12406  cnptopresti  12407  cnptoprest2  12409  cndis  12410  lmss  12415  txcnp  12440  upxp  12441  txcn  12444  txdis1cn  12447  txlm  12448  hmeoopn  12480  hmeocld  12481  xblss2ps  12573  xblss2  12574  xblm  12586  blin2  12601  blbas  12602  xmeter  12605  isxms2  12621  metss  12663  metrest  12675  xmettxlem  12678  xmettx  12679  reopnap  12707  fsumcncntop  12725  rescncf  12737  cncfss  12739  cncfco  12747  cncfmptc  12751  mulcncflem  12759  mulcncf  12760  expcncf  12761  cnopnap  12763  dedekindeulemloc  12766  dedekindeulemlu  12768  dedekindeu  12770  suplociccreex  12771  dedekindicclemloc  12775  dedekindicclemlu  12777  dedekindicclemicc  12779  ivthinclemlr  12784  ivthinclemur  12786  ivthinclemloc  12788  ivthinc  12790  limcdifap  12800  limcimo  12803  cnplimcim  12805  cnplimccntop  12808  limccnp2lem  12814  dvfgg  12826  dvcnp2cntop  12832  dvcj  12842  dvexp  12844  dveflem  12855  dvef  12856  sin0pilem1  12862  coseq0q4123  12915  cbvrald  12995  uzdcinzz  13005  bdsepnft  13085  peano5set  13138  findset  13143  bj-omtrans  13154  bj-findis  13177  strcollnft  13182  pwtrufal  13192  exmid1stab  13195  subctctexmid  13196  peano4nninf  13200  nninfalllem1  13203  nninfall  13204  nninfsellemqall  13211  nninfomnilem  13214  nninffeq  13216  exmidsbthrlem  13217  exmidsbth  13219  sbthom  13221  isomninnlem  13225  trilpolemlt1  13234