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	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ex	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem ex

Step	Hyp	Ref	Expression
1		ax-ia3 107	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2		exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜒))

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  361  exp31  362  exp32  363  exp4b  365  exp41  368  exp43  370  exp53  375  impr  377  simplbi2  383  anidms  395  syl2anc  409  pm5.74da  440  imdistanda  445  pm5.32da  448  adantl4r  509  adantl5r  517  adantl6r  518  a2and  548  impbida  586  anim12dan  590  pm2.01da  626  pm2.65da  651  mtand  655  pm5.21im  686  jao  745  jaoian  785  jaodan  787  dcim  827  stdcn  833  impidc  844  pm2.5gdc  852  con1bidc  860  con2bidc  861  con1bdc  864  pm5.18dc  869  dfandc  870  pm4.63dc  872  pm4.54dc  888  pm5.21nd  902  dcan  919  dcor  920  annimdc  922  pm4.55dc  923  pm3.11dc  942  pm3.12dc  943  prlem1  958  pm3.2an3  1161  3jcad  1163  3impia  1179  3an1rs  1198  3exp1  1202  3exp2  1204  exp520  1207  syl3anl2  1266  3jaoian  1284  3jaodan  1285  mp3anl1  1310  mp3anl2  1311  mp3anl3  1312  inegd  1351  xor3dc  1366  pm5.15dc  1368  xor2dc  1369  xornbidc  1370  xordc  1371  nbbndc  1373  biassdc  1374  dfbi3dc  1376  pm5.24dc  1377  alanimi  1436  equsexd  1708  sbequ1  1742  sbiedv  1763  ax11v2  1793  equs5or  1803  sbequi  1812  exlimdd  1845  exlimddv  1871  cbvaldva  1901  cbvexdva  1902  nfsbxyt  1917  sbcomxyyz  1946  nfsb4t  1990  eupickbi  2082  moexexdc  2084  euexex  2085  2euswapdc  2091  dvelimdc  2302  nebidc  2389  rgen2a  2489  ralimiaa  2497  ralimdaa  2501  ralrimiva  2508  ralrimdva  2515  ralrimivva  2517  ralrimdvv  2519  ralrimdvva  2520  reximdva  2537  reximssdv  2539  reximddv2  2540  rexlimiva  2547  rexlimdva  2552  rexlimdvva  2560  r19.29vva  2580  2gencl  2722  vtocldf  2740  spcimdv  2773  spcimedv  2775  rspct  2786  eqvinc  2812  eqvincg  2813  ceqex  2816  reu6  2877  eqreu  2880  sbciedf  2948  rmob  3005  csbiebt  3044  csbiedf  3045  eqelssd  3121  reupick  3365  reximdva0m  3383  ssn0  3410  rgenm  3470  eqifdc  3511  preqr1g  3701  prel12  3706  dfnfc2  3762  intssunim  3801  intab  3808  iineq2d  3841  ssiun2  3864  mpteq2da  4025  exmid01  4129  pwntru  4130  exmid1dc  4131  exmidn0m  4132  exmidsssnc  4134  exmidundif  4137  exmidundifim  4138  copsexg  4174  copsex2t  4175  sess1  4267  sess2  4268  frirrg  4280  tron  4312  onelss  4317  onintss  4320  abnexg  4375  reusv1  4387  reusv3  4389  rabxfrd  4398  iunpw  4409  ssorduni  4411  ordsson  4416  ordsucg  4426  onintrab2im  4442  onsucelsucexmidlem  4452  elirr  4464  en2lp  4477  ordsuc  4486  ordpwsucss  4490  ordtri2or2exmid  4494  reg3exmidlemwe  4501  tfisi  4509  omsinds  4543  nnpredcl  4544  sosng  4620  2optocl  4624  relop  4697  releldmb  4784  relelrnb  4785  elrnmptg  4799  elreimasng  4913  relbrcnvg  4926  trin2  4938  ssxpbm  4982  ssxp1  4983  ssxp2  4984  elxp4  5034  elxp5  5035  relresfld  5076  relcoi1  5078  iotaval  5107  iotass  5113  funmo  5146  imadif  5211  imain  5213  2elresin  5242  feu  5313  fcnvres  5314  f0rn0  5325  f1oun  5395  f1oprg  5419  relfvssunirn  5445  funbrfv  5468  funbrfv2b  5474  dffn5im  5475  dfimafn  5478  funimass4  5480  ssimaex  5490  fvmptssdm  5513  fvmptf  5521  elfvmptrab1  5523  fvimacnv  5543  funimass3  5544  elpreima  5547  elrnrexdm  5567  eldmrexrn  5569  dffo4  5576  dffo5  5577  fmpt  5578  fmptdf  5585  ffvresb  5591  resflem  5592  fmptco  5594  fsn  5600  funfvima  5657  funfvima2  5658  f1mpt  5680  f1imass  5683  f1ocnvfvrneq  5691  foeqcnvco  5699  f1eqcocnv  5700  fliftfun  5705  fliftf  5708  isopolem  5731  isosolem  5733  eusvobj2  5768  acexmidlemab  5776  oprabid  5811  ovidi  5897  ovg  5917  suppssfv  5986  suppssov1  5987  funrnex  6020  f1dmex  6022  oprabexd  6033  fo2ndresm  6068  oprssdmm  6077  op1steq  6085  dfoprab3  6097  fo2ndf  6132  f1o2ndf1  6133  poxp  6137  spc2ed  6138  f1od2  6140  rbropapd  6147  reldmtpos  6158  rntpos  6162  tposf2  6173  tposf12  6174  issmo2  6194  smores  6197  smoiso  6207  tfrlem9  6224  tfrlemibacc  6231  tfrlemibfn  6233  tfrlemi14d  6238  tfrexlem  6239  tfr1onlembacc  6247  tfr1onlembfn  6249  tfr1onlemres  6254  tfri1dALT  6256  tfrcllembacc  6260  tfrcllembfn  6262  tfrcllemres  6267  tfrcl  6269  rdgivallem  6286  frecabcl  6304  frecrdg  6313  oawordi  6373  nnmcom  6393  nnsucelsuc  6395  nntri3or  6397  nnsucuniel  6399  nntri1  6400  nnsseleq  6405  nntr2  6407  dcdifsnid  6408  nnaordi  6412  nnmord  6421  nnaordex  6431  nnm00  6433  ertr  6452  erex  6461  iserd  6463  iinerm  6509  erinxp  6511  qsel  6514  qliftfun  6519  qliftfund  6520  2ecoptocl  6525  brecop  6527  mapss  6593  ixpssmap2g  6629  ixpssmapg  6630  dom2lem  6674  fundmen  6708  unen  6718  enm  6722  xpdom2  6733  fopwdom  6738  xpf1o  6746  mapen  6748  mapxpen  6750  ssenen  6753  phplem4  6757  nneneq  6759  snnen2og  6761  phplem4dom  6764  nndomo  6766  phpm  6767  phplem4on  6769  fidifsnen  6772  dif1enen  6782  fin0  6787  fin0or  6788  findcard2  6791  findcard2s  6792  findcard2d  6793  findcard2sd  6794  ac6sfi  6800  fimax2gtri  6803  finexdc  6804  en2eqpr  6809  onunsnss  6813  unfidisj  6818  undifdcss  6819  undifdc  6820  fiintim  6825  xpfi  6826  fisseneq  6828  ssfirab  6830  fnfi  6833  iunfidisj  6842  f1finf1o  6843  en1eqsnbi  6845  fidcenum  6852  isbth  6863  ssfii  6870  fieq0  6872  eqsupti  6891  suplub2ti  6896  isotilem  6901  supisoex  6904  eqinfti  6915  inflbti  6919  ordiso2  6928  djulclb  6948  updjudhf  6972  updjud  6975  difinfsn  6993  difinfinf  6994  ctmlemr  7001  ctm  7002  ctssdclemn0  7003  ctssdccl  7004  ctssdc  7006  enumct  7008  enomnilem  7018  finomni  7020  exmidomniim  7021  exmidomni  7022  fodjuomnilemdc  7024  fodjuomnilemres  7028  nnnninf  7031  ismkvnex  7037  mkvprop  7040  fodjumkvlemres  7041  enmkvlem  7043  enwomnilem  7050  pm54.43  7063  pr2nelem  7064  pr2ne  7065  exmidfodomrlemim  7074  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  acfun  7080  ccfunen  7096  cc1  7097  cc3  7100  cc4f  7101  cc4n  7103  mulcanpig  7167  nlt1pig  7173  addcmpblnq  7199  ltsonq  7230  ltexnqq  7240  prarloclemarch2  7251  enq0tr  7266  addcmpblnq0  7275  addnq0mo  7279  mulnq0mo  7280  prcdnql  7316  prcunqu  7317  prarloclemlo  7326  prarloclem3step  7328  prarloclem3  7329  genpdflem  7339  genpelvl  7344  genpelvu  7345  genpcdl  7351  genpcuu  7352  genprndl  7353  genprndu  7354  genpdisj  7355  addnqprllem  7359  addnqprulem  7360  addlocprlemeq  7365  addlocprlemgt  7366  nqprloc  7377  nqprl  7383  nqpru  7384  addnqprlemrl  7389  addnqprlemru  7390  addnqprlemfl  7391  addnqprlemfu  7392  prmuloc  7398  prmuloc2  7399  mullocpr  7403  mulnqprlemrl  7405  mulnqprlemru  7406  mulnqprlemfl  7407  mulnqprlemfu  7408  distrlem4prl  7416  distrlem4pru  7417  ltprordil  7421  1idprl  7422  1idpru  7423  ltpopr  7427  ltsopr  7428  ltaddpr  7429  ltexprlemm  7432  ltexprlemlol  7434  ltexprlemupu  7436  ltexprlemdisj  7438  ltexprlemloc  7439  ltexprlemrl  7442  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  addcanprg  7448  ltaprg  7451  recexprlemlol  7458  recexprlemdisj  7462  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  aptiprleml  7471  aptiprlemu  7472  ltmprr  7474  archpr  7475  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemrnd  7482  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgprlemnkj  7498  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemrnd  7505  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlemlim  7513  caucvgprprlemnkltj  7521  caucvgprprlemnkeqj  7522  caucvgprprlemnjltk  7523  caucvgprprlemml  7526  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemrnd  7533  caucvgprprlemloc  7535  caucvgprprlemexbt  7538  caucvgprprlemexb  7539  caucvgprprlemlim  7543  suplocexprlemrl  7549  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemloc  7553  suplocexprlemex  7554  suplocexprlemlub  7556  mulcmpblnrlemg  7572  addsrmo  7575  mulsrmo  7576  ltsrprg  7579  srpospr  7615  caucvgsrlemgt1  7627  map2psrprg  7637  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  cnm  7664  pitonn  7680  nntopi  7726  axcaucvglemcau  7730  axcaucvglemres  7731  axpre-suploclemres  7733  lelttr  7876  ltletr  7877  readdcan  7926  cnegexlem1  7961  cnegexlem2  7962  addid0  8159  lelttrdi  8212  add20  8260  eqord1  8269  recexre  8364  inelr  8370  rimul  8371  apreap  8373  ltmul1  8378  cru  8388  apreim  8389  apirr  8391  apsym  8392  apcotr  8393  apadd1  8394  apneg  8397  mulext1  8398  msqge0  8402  mulge0  8405  apti  8408  ltleap  8418  aprcl  8432  recexap  8438  mulap0b  8440  mul0eqap  8455  recgt0  8632  prodgt02  8635  prodge02  8637  lemul12b  8643  lemul12a  8644  nnrecgt0  8782  addltmul  8980  nominpos  8981  elnnz  9088  peano2z  9114  zaddcllempos  9115  zaddcl  9118  zletric  9122  zlelttric  9123  zltnle  9124  zleloe  9125  zrevaddcl  9128  nzadd  9130  zdceq  9150  zdcle  9151  zdclt  9152  nn0n0n1ge2b  9154  nn0lt2  9156  zextle  9166  peano5uzti  9183  uzind2  9187  fzind  9190  fnn0ind  9191  nn0ind-raph  9192  btwnz  9194  eluzuzle  9358  uz11  9372  eluzp1m1  9373  supinfneg  9417  infsupneg  9418  lbzbi  9435  qapne  9458  qreccl  9461  qrevaddcl  9463  irradd  9465  irrmul  9466  elpq  9467  ledivge1le  9543  nn0ledivnn  9584  xrlelttr  9619  xrltletr  9620  npnflt  9628  nmnfgt  9631  xnn0lenn0nn0  9678  xnn0xadd0  9680  xleadd1  9688  xle2add  9692  xposdif  9695  xlesubadd  9696  ixxss1  9717  ixxss2  9718  ixxss12  9719  iccid  9738  elioc2  9749  elico2  9750  elicc2  9751  fznlem  9852  fzn  9853  fzen  9854  0fz1  9856  uzsubsubfz  9858  fzopth  9872  fzss1  9874  fzss2  9875  elfz1b  9901  uzsplit  9903  fzm1  9911  fznuz  9913  fzrevral  9916  elfz0ubfz0  9933  elfz0fzfz0  9934  fz0fzelfz0  9935  difelfzle  9942  1fv  9947  fzoss1  9979  fzosplit  9985  fzouzsplit  9987  fzonmapblen  9995  fzofzim  9996  eluzgtdifelfzo  10005  elfzodifsumelfzo  10009  elfzom1p1elfzo  10022  ssfzo12  10032  ssfzo12bi  10033  fzofzp1b  10036  elfzonelfzo  10038  subfzo0  10050  qtri3or  10051  qletric  10052  qlelttric  10053  qltnle  10054  qdceq  10055  exbtwnzlemstep  10056  exbtwnzlemshrink  10057  exbtwnzlemex  10058  exbtwnz  10059  rebtwn2zlemstep  10061  rebtwn2z  10063  ioom  10069  ico0  10070  ioc0  10071  flltdivnn0lt  10108  flqeqceilz  10122  modqid2  10155  modqmuladd  10170  modqmuladdim  10171  modqmuladdnn0  10172  modqm1p1mod0  10179  modaddmodlo  10192  modfzo0difsn  10199  addmodlteq  10202  frec2uzuzd  10206  frec2uzltd  10207  frec2uzlt2d  10208  frec2uzrand  10209  frec2uzf1od  10210  frec2uzrdg  10213  frecuzrdgtcl  10216  frecuzrdgdomlem  10221  frecuzrdgfunlem  10223  frecfzennn  10230  uzennn  10240  uzsinds  10246  seq3clss  10271  iseqf1olemqf1o  10297  seq3f1olemp  10306  seq3id3  10311  seq3id  10312  seq3z  10315  ser3ge0  10321  expcl2lemap  10336  leexp2r  10378  leexp1a  10379  zesq  10441  expnbnd  10446  nn0opthlem2d  10499  nn0opthd  10500  facdiv  10516  facndiv  10517  facwordi  10518  faclbnd  10519  faclbnd6  10522  facubnd  10523  bcval4  10530  bcpasc  10544  bccl  10545  fiinfnf1o  10564  fihashf1rn  10567  hashunlem  10582  fiprsshashgt1  10595  hashfzo  10600  hashfzp1  10602  hashxp  10604  hashfacen  10611  zfz1iso  10616  seq3coll  10617  ovshftex  10623  reim0b  10666  cjap  10710  caucvgrelemcau  10784  caucvgre  10785  cvg1nlemres  10789  r19.29uz  10796  r19.2uz  10797  recvguniq  10799  sqrt0  10808  resqrexlemover  10814  resqrexlemdecn  10816  resqrexlemlo  10817  resqrexlemcalc3  10820  resqrexlemglsq  10826  resqrexlemga  10827  rsqrmo  10831  sqrtsq  10848  abs00ap  10866  absnid  10877  qabsor  10879  absexpzap  10884  abs3lem  10915  cau3lem  10918  caubnd2  10921  icodiamlt  10984  maxleim  11009  maxabslemlub  11011  maxabslemval  11012  fimaxre2  11030  negfi  11031  minmax  11033  xrmaxleim  11045  xrmaxiflemlub  11049  xrmaxiflemval  11051  xrminmax  11066  clim  11082  climuni  11094  climcn1  11109  climcn2  11110  mulcn2  11113  iserex  11140  climcau  11148  climcaucn  11152  sumrbdclem  11178  fsum3cvg  11179  summodclem2a  11182  zsumdc  11185  fsum3  11188  isumz  11190  fsumf1o  11191  fisumss  11193  fsum3cvg3  11197  fsumsplit  11208  fsum2dlemstep  11235  fsumconst  11255  modfsummod  11259  fsum00  11263  fsumabs  11266  fsumrelem  11272  fsumiun  11278  bcxmas  11290  isumsplit  11292  divcnv  11298  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  mertenslem2  11337  ntrivcvgap  11349  prodrbdclem  11372  prodmodclem2a  11377  prodmodc  11379  zproddc  11380  efexp  11425  efieq1re  11514  eirrap  11520  dvdsval2  11532  moddvds  11538  dvds0  11544  absdvdsb  11547  dvdsabsb  11548  dvdsmul1  11551  dvdscmul  11556  dvdsmulc  11557  dvds2ln  11562  dvds2add  11563  dvds2sub  11564  dvdslelemd  11577  dvdsleabs2  11580  dvds1  11587  dvdsext  11589  fzo0dvdseq  11591  dvdsfac  11594  mulmoddvds  11597  odd2np1  11606  oddge22np1  11614  evennn02n  11615  evennn2n  11616  mulsucdiv2z  11618  sqoddm1div8z  11619  ltoddhalfle  11626  halfleoddlt  11627  m1expo  11633  nn0ehalf  11636  nn0o  11640  nn0oddm1d2  11642  nnoddm1d2  11643  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  flodddiv4  11667  zsupcllemstep  11674  dvdsbnd  11681  dvdslegcd  11689  gcdeq0  11701  gcd0id  11703  gcdneg  11706  gcdaddm  11708  gcdabs  11712  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlemzz  11726  bezoutlemaz  11727  bezoutlembz  11728  bezoutlembi  11729  bezoutlemeu  11731  bezoutlemle  11732  bezoutlemsup  11733  dvdsgcd  11736  dfgcd2  11738  rppwr  11752  dvdssqlem  11754  bezoutr1  11757  algfx  11769  eucalglt  11774  eucalgcvga  11775  lcmledvds  11787  lcmeq0  11788  lcmneg  11791  lcmabs  11793  lcmgcdlem  11794  lcmdvds  11796  lcmgcdeq  11800  coprmgcdb  11805  ncoprmgcdne1b  11806  coprmdvds  11809  qredeq  11813  qredeu  11814  rpdvds  11816  divgcdcoprm0  11818  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  isprm2lem  11833  prmind2  11837  dvdsnprmd  11842  divgcdodd  11857  coprm  11858  isprm6  11861  prmfac1  11866  rpexp  11867  sqrt2irr  11876  pw2dvdseu  11882  sqrt2irrap  11894  nonsq  11921  hashdvds  11933  phimullem  11937  ennnfonelemk  11949  ennnfoneleminc  11960  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemhom  11964  ennnfonelemrnh  11965  ennnfonelemdm  11969  ennnfone  11974  exmidunben  11975  ctinfom  11977  ctinf  11979  enctlem  11981  unct  11991  omctfn  11992  uniopn  12207  toponcomb  12234  bastg  12269  tgcl  12272  tgdom  12280  en1top  12285  tgss3  12286  bastop2  12292  epttop  12298  iuncld  12323  isopn3  12333  neiint  12353  neisspw  12356  0nnei  12361  neipsm  12362  opnneissb  12363  opnssneib  12364  tpnei  12368  neiuni  12369  opnneiid  12372  neissex  12373  ssrest  12390  tgcn  12416  tgcnp  12417  iscnp4  12426  cnpnei  12427  cnntr  12433  cnss1  12434  cnss2  12435  cncnp2m  12439  cnrest2  12444  cnrest2r  12445  cnptopresti  12446  cnptoprest2  12448  cndis  12449  lmss  12454  txcnp  12479  upxp  12480  txcn  12483  txdis1cn  12486  txlm  12487  hmeoopn  12519  hmeocld  12520  xblss2ps  12612  xblss2  12613  xblm  12625  blin2  12640  blbas  12641  xmeter  12644  isxms2  12660  metss  12702  metrest  12714  xmettxlem  12717  xmettx  12718  reopnap  12746  fsumcncntop  12764  rescncf  12776  cncfss  12778  cncfco  12786  cncfmptc  12790  mulcncflem  12798  mulcncf  12799  expcncf  12800  cnopnap  12802  dedekindeulemloc  12805  dedekindeulemlu  12807  dedekindeu  12809  suplociccreex  12810  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicclemicc  12818  ivthinclemlr  12823  ivthinclemur  12825  ivthinclemloc  12827  ivthinc  12829  limcdifap  12839  limcimo  12842  cnplimcim  12844  cnplimccntop  12847  limccnp2lem  12853  dvfgg  12865  dvcnp2cntop  12871  dvcj  12881  dvexp  12883  dveflem  12895  dvef  12896  eflt  12904  sin0pilem1  12910  coseq0q4123  12963  cos11  12982  logbgcd1irr  13092  logbgcd1irrap  13095  cbvrald  13166  uzdcinzz  13176  bdsepnft  13256  peano5set  13309  findset  13314  bj-omtrans  13325  bj-findis  13348  strcollnft  13353  pwtrufal  13365  exmid1stab  13368  subctctexmid  13369  peano4nninf  13375  nninfalllem1  13378  nninfall  13379  nninfsellemqall  13386  nninfomnilem  13389  nninffeq  13391  exmidsbthrlem  13392  exmidsbth  13394  sbthom  13396  isomninnlem  13400  trilpolemlt1  13409  apdiff  13416  ismkvnnlem  13419  neapmkvlem  13424