Theorem ex 113

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 106	. 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 102

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

This theorem is referenced by:  expcom  114  bi3  117  expd  254  impancom  256  expimpd  355  exp31  356  exp32  357  exp4b  359  exp41  362  exp43  364  exp53  369  impr  371  simplbi2  377  anidms  389  syl2anc  403  pm5.74da  431  imdistanda  436  pm5.32da  439  impbida  560  anim12dan  564  pm2.01da  597  pm2.65da  619  mtand  623  pm5.21im  644  jao  704  jaoian  741  jaodan  743  impidc  788  pm2.5dc  796  con1bidc  801  con2bidc  802  con1bdc  805  pm5.18dc  810  dfandc  811  pm4.63dc  813  dcim  817  pm4.54dc  838  pm5.21nd  858  dcan  875  dcor  876  annimdc  878  pm4.55dc  879  pm3.11dc  898  pm3.12dc  899  prlem1  914  pm3.2an3  1117  3jcad  1119  3impia  1135  3an1rs  1150  3exp1  1154  3exp2  1156  exp520  1159  syl3anl2  1218  3jaoian  1236  3jaodan  1237  mp3anl1  1262  mp3anl2  1263  mp3anl3  1264  inegd  1303  xor3dc  1318  pm5.15dc  1320  xor2dc  1321  xornbidc  1322  xordc  1323  nbbndc  1325  biassdc  1326  dfbi3dc  1328  pm5.24dc  1329  alanimi  1388  equsexd  1657  sbequ1  1691  sbiedv  1712  ax11v2  1741  equs5or  1751  sbequi  1760  exlimdd  1793  exlimddv  1819  cbvaldva  1844  cbvexdva  1845  nfsbxyt  1860  sbcomxyyz  1887  nfsb4t  1931  eupickbi  2023  moexexdc  2025  euexex  2026  2euswapdc  2032  dvelimdc  2238  nebidc  2325  rgen2a  2417  ralimiaa  2425  ralimdaa  2428  ralrimiva  2434  ralrimdva  2441  ralrimivva  2443  ralrimdvv  2445  ralrimdvva  2446  reximdva  2463  reximddv2  2465  rexlimiva  2472  rexlimdva  2477  rexlimdvva  2484  r19.29vva  2500  2gencl  2632  vtocldf  2650  spcimdv  2682  spcimedv  2684  rspct  2694  eqvinc  2718  eqvincg  2719  ceqex  2722  reu6  2781  eqreu  2784  sbciedf  2849  rmob  2906  csbiebt  2942  csbiedf  2943  reupick  3248  reximdva0m  3263  ssn0  3286  rgenm  3343  preqr1g  3558  prel12  3563  dfnfc2  3619  intssunim  3658  intab  3665  iineq2d  3698  ssiun2  3721  mpteq2da  3867  trintssmOLD  3892  copsexg  3999  copsex2t  4000  sess1  4092  sess2  4093  frirrg  4105  tron  4137  onelss  4142  onintss  4145  reusv1  4208  reusv3  4210  rabxfrd  4219  iunpw  4229  ssorduni  4231  ordsson  4236  ordsucg  4246  onintrab2im  4262  onsucelsucexmidlem  4272  elirr  4284  en2lp  4297  ordsuc  4306  ordpwsucss  4310  ordtri2or2exmid  4314  reg3exmidlemwe  4321  tfisi  4328  sosng  4431  2optocl  4435  relop  4504  xpid11m  4575  releldmb  4589  relelrnb  4590  elrnmptg  4604  elreimasng  4711  relbrcnvg  4724  trin2  4736  ssxpbm  4776  ssxp1  4777  ssxp2  4778  elxp4  4828  elxp5  4829  relresfld  4867  relcoi1  4869  iotaval  4898  iotass  4904  funmo  4937  imadif  4999  imain  5001  2elresin  5030  feu  5092  fcnvres  5093  f1oun  5166  f1oprg  5188  relfvssunirn  5211  funbrfv  5233  funbrfv2b  5239  dffn5im  5240  dfimafn  5243  funimass4  5245  ssimaex  5255  fvmptssdm  5276  fvmptf  5284  fvimacnv  5303  funimass3  5304  elpreima  5307  elrnrexdm  5327  eldmrexrn  5329  dffo4  5336  dffo5  5337  fmpt  5340  ffvresb  5349  fmptco  5351  fsn  5356  funfvima  5411  funfvima2  5412  f1mpt  5431  f1imass  5434  f1ocnvfvrneq  5442  foeqcnvco  5450  f1eqcocnv  5451  fliftfun  5456  fliftf  5459  isopolem  5481  isosolem  5483  eusvobj2  5518  acexmidlemab  5526  oprabid  5557  ovidi  5639  ovg  5659  suppssfv  5728  suppssov1  5729  funrnex  5761  f1dmex  5763  oprabexd  5774  fo2ndresm  5809  op1steq  5825  dfoprab3  5837  fo2ndf  5868  f1o2ndf1  5869  poxp  5873  spc2ed  5874  f1od2  5876  isprmpt2  5881  reldmtpos  5891  rntpos  5895  tposf2  5906  tposf12  5907  issmo2  5927  smores  5930  smoiso  5940  tfrlem9  5958  tfrlemibacc  5963  tfrlemibfn  5965  tfrlemi14d  5970  tfrexlem  5971  rdgivallem  5991  frecsuclem3  6013  frecrdg  6015  freccl  6016  oawordi  6072  nnmcom  6091  nnsucelsuc  6093  nntri3or  6095  nntri1  6097  nnsseleq  6102  nndifsnid  6103  nnaordi  6104  nnmord  6113  nnaordex  6123  nnm00  6125  ertr  6144  erex  6153  iserd  6155  iinerm  6201  erinxp  6203  qsel  6206  qliftfun  6211  qliftfund  6212  2ecoptocl  6217  brecop  6219  dom2lem  6275  fundmen  6309  unen  6316  enm  6317  xpdom2  6328  fopwdom  6333  phplem4  6341  nneneq  6343  snnen2og  6345  phplem4dom  6348  nndomo  6350  phpm  6351  phplem4on  6353  fidifsnen  6355  fidifsnid  6356  fin0  6369  fin0or  6370  findcard2  6373  findcard2s  6374  findcard2d  6375  findcard2sd  6376  ac6sfi  6379  en2eqpr  6380  onunsnss  6383  fnfi  6388  eqsupti  6409  suplub2ti  6414  isotilem  6419  supisoex  6422  eqinfti  6433  inflbti  6437  ordiso2  6446  pm54.43  6459  pr2nelem  6460  pr2ne  6461  mulcanpig  6525  nlt1pig  6531  addcmpblnq  6557  ltsonq  6588  ltexnqq  6598  prarloclemarch2  6609  enq0tr  6624  addcmpblnq0  6633  addnq0mo  6637  mulnq0mo  6638  prcdnql  6674  prcunqu  6675  prarloclemlo  6684  prarloclem3step  6686  prarloclem3  6687  genpdflem  6697  genpelvl  6702  genpelvu  6703  genpcdl  6709  genpcuu  6710  genprndl  6711  genprndu  6712  genpdisj  6713  addnqprllem  6717  addnqprulem  6718  addlocprlemeq  6723  addlocprlemgt  6724  nqprloc  6735  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  addnqprlemfl  6749  addnqprlemfu  6750  prmuloc  6756  prmuloc2  6757  mullocpr  6761  mulnqprlemrl  6763  mulnqprlemru  6764  mulnqprlemfl  6765  mulnqprlemfu  6766  distrlem4prl  6774  distrlem4pru  6775  ltprordil  6779  1idprl  6780  1idpru  6781  ltpopr  6785  ltsopr  6786  ltaddpr  6787  ltexprlemm  6790  ltexprlemlol  6792  ltexprlemupu  6794  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  addcanprg  6806  ltaprg  6809  recexprlemlol  6816  recexprlemdisj  6820  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  aptiprleml  6829  aptiprlemu  6830  ltmprr  6832  archpr  6833  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemopu  6838  cauappcvgprlemrnd  6840  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemnkj  6856  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemopu  6861  caucvgprlemrnd  6863  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlemlim  6871  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnjltk  6881  caucvgprprlemml  6884  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemrnd  6891  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlemexb  6897  caucvgprprlemlim  6901  mulcmpblnrlemg  6917  addsrmo  6920  mulsrmo  6921  ltsrprg  6924  srpospr  6959  caucvgsrlemgt1  6971  pitonn  7016  nntopi  7060  axcaucvglemcau  7064  axcaucvglemres  7065  lelttr  7199  ltletr  7200  readdcan  7248  cnegexlem1  7283  cnegexlem2  7284  addid0  7477  lelttrdi  7530  add20  7578  recexre  7678  inelr  7684  rimul  7685  apreap  7687  ltmul1  7692  cru  7702  apreim  7703  apirr  7705  apsym  7706  apcotr  7707  apadd1  7708  apneg  7711  mulext1  7712  msqge0  7716  mulge0  7719  apti  7722  ltleap  7730  recexap  7743  mulap0b  7745  recgt0  7928  prodgt02  7931  prodge02  7933  lemul12b  7939  lemul12a  7940  nnrecgt0  8076  addltmul  8267  nominpos  8268  elnnz  8361  peano2z  8387  zaddcllempos  8388  zaddcl  8391  zletric  8395  zlelttric  8396  zltnle  8397  zleloe  8398  zrevaddcl  8401  nzadd  8403  zdceq  8423  zdcle  8424  zdclt  8425  nn0n0n1ge2b  8427  nn0lt2  8429  zextle  8438  peano5uzti  8455  uzind2  8459  fzind  8462  fnn0ind  8463  nn0ind-raph  8464  btwnz  8466  eluzuzle  8627  uz11  8641  eluzp1m1  8642  supinfneg  8683  infsupneg  8684  lbzbi  8701  qapne  8724  qreccl  8727  qrevaddcl  8729  irradd  8731  irrmul  8732  ledivge1le  8803  nn0ledivnn  8838  xrlelttr  8876  xrltletr  8877  ixxss1  8927  ixxss2  8928  ixxss12  8929  iccid  8948  elioc2  8959  elico2  8960  elicc2  8961  fznlem  9060  fzn  9061  fzen  9062  0fz1  9064  uzsubsubfz  9066  fzopth  9079  fzss1  9081  fzss2  9082  elfz1b  9107  uzsplit  9109  fzm1  9117  fznuz  9119  fzrevral  9122  elfz0ubfz0  9136  elfz0fzfz0  9137  fz0fzelfz0  9138  difelfzle  9145  1fv  9149  fzoss1  9180  fzosplit  9186  fzouzsplit  9188  fzonmapblen  9196  fzofzim  9197  eluzgtdifelfzo  9206  elfzodifsumelfzo  9210  elfzom1p1elfzo  9223  ssfzo12  9233  ssfzo12bi  9234  fzofzp1b  9237  elfzonelfzo  9239  subfzo0  9251  qtri3or  9252  qletric  9253  qlelttric  9254  qltnle  9255  qdceq  9256  qbtwnzlemstep  9257  qbtwnzlemex  9259  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2z  9263  ioom  9269  ico0  9270  ioc0  9271  flltdivnn0lt  9306  flqeqceilz  9320  modqid2  9353  modqmuladd  9368  modqmuladdim  9369  modqmuladdnn0  9370  modqm1p1mod0  9377  modaddmodlo  9390  modfzo0difsn  9397  addmodlteq  9400  frec2uzzd  9402  frec2uzuzd  9404  frec2uzltd  9405  frec2uzlt2d  9406  frec2uzrand  9407  frec2uzf1od  9408  frec2uzrdg  9411  frecuzrdgfn  9414  frecfzennn  9419  uzsinds  9428  iseqid3s  9466  iseqid  9467  iseqz  9469  expival  9478  expcl2lemap  9488  leexp2r  9530  leexp1a  9531  zesq  9591  expnbnd  9596  nn0opthlem2d  9648  nn0opthd  9649  facdiv  9665  facndiv  9666  facwordi  9667  faclbnd  9668  faclbnd6  9671  facubnd  9672  bcval4  9679  bcpasc  9693  bccl  9694  ovshftex  9707  reim0b  9749  cjap  9793  caucvgrelemcau  9866  caucvgre  9867  cvg1nlemres  9871  r19.29uz  9878  r19.2uz  9879  recvguniq  9881  sqrt0  9890  resqrexlemover  9896  resqrexlemdecn  9898  resqrexlemlo  9899  resqrexlemcalc3  9902  resqrexlemglsq  9908  resqrexlemga  9909  rsqrmo  9913  sqrtsq  9930  abs00ap  9948  absnid  9959  qabsor  9961  absexpzap  9966  abs3lem  9997  cau3lem  10000  caubnd2  10003  icodiamlt  10066  maxleim  10091  maxabslemlub  10093  maxabslemval  10094  fimaxre2  10109  negfi  10110  minmax  10112  clim  10120  climuni  10132  climcn1  10147  climcn2  10148  mulcn2  10151  iiserex  10177  climcau  10184  climcaucn  10188  dvdsval2  10198  moddvds  10204  dvds0  10210  absdvdsb  10213  dvdsabsb  10214  dvdsmul1  10217  dvdscmul  10222  dvdsmulc  10223  dvds2ln  10228  dvds2add  10229  dvds2sub  10230  dvdslelemd  10243  dvdsleabs2  10246  dvds1  10253  dvdsext  10255  fzo0dvdseq  10257  dvdsfac  10260  mulmoddvds  10263  odd2np1  10272  oddge22np1  10281  evennn02n  10282  evennn2n  10283  mulsucdiv2z  10285  sqoddm1div8z  10286  ltoddhalfle  10293  halfleoddlt  10294  m1expo  10300  nn0ehalf  10303  nn0o  10307  nn0oddm1d2  10309  nnoddm1d2  10310  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  flodddiv4  10334  zsupcllemstep  10341  dvdsbnd  10348  dvdslegcd  10356  gcdeq0  10368  gcd0id  10370  gcdneg  10373  gcdaddm  10375  gcdabs  10379  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemzz  10391  bezoutlemaz  10392  bezoutlembz  10393  bezoutlembi  10394  bezoutlemeu  10396  bezoutlemle  10397  bezoutlemsup  10398  dvdsgcd  10401  dfgcd2  10403  rppwr  10417  dvdssqlem  10419  bezoutr1  10422  ialgfx  10434  eucalglt  10439  eucialgcvga  10440  lcmledvds  10452  lcmeq0  10453  lcmneg  10456  lcmabs  10458  lcmgcdlem  10459  lcmdvds  10461  lcmgcdeq  10465  coprmgcdb  10470  ncoprmgcdne1b  10471  coprmdvds  10474  qredeq  10478  qredeu  10479  rpdvds  10481  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  isprm2lem  10498  prmind2  10502  dvdsnprmd  10507  divgcdodd  10522  coprm  10523  isprm6  10526  prmfac1  10531  rpexp  10532  sqrt2irr  10541  pw2dvdseu  10546  sqrt2irrap  10558  cbvrald  10598  bdsepnft  10678  peano5set  10735  findset  10740  bj-omtrans  10751  bj-findis  10774  strcollnft  10779