Theorem expimpd 453

Description: Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)

Hypothesis

Ref	Expression
expimpd.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
expimpd	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem expimpd

Step	Hyp	Ref	Expression
1		expimpd.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 412	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 410	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  ornld  1062  3impia  1118  ralrimdva  3138  disjiun  5074  reusv3  5340  euotd  5459  swopo  5541  sotr3  5571  wereu2  5619  poirr2  6079  sossfld  6142  reuop  6249  frpomin  6296  oneqmini  6368  suctr  6403  elpreima  7002  fmptco  7074  isofrlem  7286  onmindif2  7752  resf1extb  7876  mptcnfimad  7930  frxp  8067  fnse  8074  suppss  8135  tposfo2  8190  wfr3g  8260  tz7.48-2  8372  omeulem1  8508  omeu  8511  nnaordex  8565  eldifsucnn  8591  pssnn  9094  onomeneq  9139  fodomfib  9230  fodomfibOLD  9232  dffi3  9335  supmo  9356  supnub  9366  infglb  9395  infnlb  9397  infmo  9401  infsupprpr  9410  cantnfle  9581  cantnflem1  9599  epfrs  9641  frr3g  9669  updjud  9847  alephord2i  9988  cardinfima  10008  aceq3lem  10031  dfac2b  10042  dfac12lem2  10056  axdc2lem  10359  ttukeylem6  10425  alephval2  10484  fpwwe2lem11  10553  fpwwe2lem12  10554  prlem934  10945  reclem4pr  10962  suplem1pr  10964  letr  11229  sup2  12101  uzind  12610  ledivge1le  13004  xrletr  13098  xltnegi  13157  xlemul1a  13229  ixxssixx  13301  difreicc  13426  flval3  13763  fsequb  13926  seqf1olem1  13992  expnegz  14047  hash2prd  14426  ccatrcl1  14546  relexprelg  14989  shftlem  15019  rexuzre  15304  cau3lem  15306  caubnd2  15309  caubnd  15310  climrlim2  15498  climuni  15503  2clim  15523  o1co  15537  rlimno1  15605  climbdd  15623  caurcvg  15628  summolem2  15667  summo  15668  zsum  15669  fsumf1o  15674  fsumss  15676  fsumcl2lem  15682  fsumadd  15691  fsummulc2  15735  fsumconst  15741  fsumrelem  15759  prodmolem2  15889  prodmo  15890  zprod  15891  fprodf1o  15900  fprodss  15902  fprodcl2lem  15904  fprodmul  15914  fproddiv  15915  fprodconst  15932  fprodn0  15933  dfgcd2  16504  lcmfunsnlem2  16598  coprmproddvdslem  16620  cncongrprm  16688  prmpwdvds  16864  infpnlem1  16870  1arith  16887  vdwapun  16934  vdwlem11  16951  vdwnnlem2  16956  ramz  16985  ramcl  16989  prmlem0  17065  firest  17384  catpropd  17664  initoid  17957  termoid  17958  initoeu2lem1  17970  pltnle  18291  pltletr  18296  pospo  18298  psss  18535  isgrpid2  18941  f1omvdco2  19412  pgpfi  19569  frgpnabllem1  19837  gsumval3eu  19868  gsumzres  19873  gsumzcl2  19874  gsumzf1o  19876  gsumzaddlem  19885  gsumconst  19898  gsumzmhm  19901  gsumzoppg  19908  ablfaclem3  20053  dvdsrtr  20337  dvdsrmul1  20338  unitgrp  20352  domnmuln0  20675  lspsolvlem  21130  gsumfsum  21422  nzerooringczr  21468  obslbs  21718  gsummoncoe1  22282  pf1ind  22329  dmatscmcl  22477  scmatmulcl  22492  smatvscl  22498  mdetdiaglem  22572  cpmatinvcl  22691  mp2pm2mplem4  22783  cpmadugsumlemF  22850  eltg3  22936  tgidm  22954  neindisj  23091  tgrest  23133  restcld  23146  tgcn  23226  lmcnp  23278  iunconnlem  23401  2ndcredom  23424  2ndc1stc  23425  1stcrest  23427  2ndcrest  23428  2ndcdisj  23430  nllyrest  23460  nllyidm  23463  lfinpfin  23498  locfincmp  23500  ptpjpre1  23545  ptuni2  23550  ptbasin  23551  ptbasfi  23555  txbasval  23580  ptpjopn  23586  ptclsg  23589  dfac14lem  23591  xkoccn  23593  txcnp  23594  ptcnplem  23595  ptcnp  23596  txtube  23614  txcmplem1  23615  txcmplem2  23616  tx2ndc  23625  txkgen  23626  xkoco1cn  23631  xkoco2cn  23632  xkococnlem  23633  xkococn  23634  xkoinjcn  23661  qtoprest  23691  kqsat  23705  kqcldsat  23707  isfild  23832  fbunfip  23843  fgabs  23853  filconn  23857  fbasrn  23858  filufint  23894  elfm2  23922  elfm3  23924  fmfnfm  23932  hausflimi  23954  cnpflfi  23973  ptcmplem2  24027  tmdgsum2  24070  cldsubg  24085  qustgpopn  24094  ustfilxp  24187  bldisj  24372  xbln0  24388  blssps  24398  blss  24399  blssexps  24400  blssex  24401  blcls  24480  metcnp3  24514  icccmplem2  24798  mpomulcn  24843  cnheibor  24931  iscau4  25255  cmssmscld  25326  ovolshftlem2  25486  ovolicc2lem5  25497  dyadmax  25574  mbfi1fseqlem4  25694  mbfi1flimlem  25698  lhop1lem  25990  dvfsumrlim  26010  aalioulem3  26313  ulmcn  26379  radcnvlt1  26398  pilem2  26433  efopn  26638  cxpeq0  26658  cxpmul2z  26671  cxpcn3lem  26728  xrlimcnp  26949  vmappw  27097  fsumvma  27195  dchrptlem1  27246  lgsqr  27333  lgsdchrval  27336  2lgslem3  27386  2sqlem6  27405  2sqlem7  27406  2sqreultlem  27429  2sqreunnltlem  27432  pntlem3  27591  pntleml  27593  ltsval2  27639  nosupno  27686  nosupbnd1lem5  27695  noinfno  27701  lestr  27745  madebdayim  27899  ltslpss  27919  negsid  28052  noseqinds  28304  brbtwn  28987  brcgr  28988  axcontlem8  29059  nbumgrvtx  29434  cusgrfilem2  29545  1loopgrnb0  29591  uspgr2wlkeq  29734  wlklenvclwlk  29742  upgrwlkdvdelem  29824  uspgrn2crct  29896  0enwwlksnge1  29952  usgr2wspthons3  30055  clwwlkccatlem  30079  clwlkclwwlkf  30098  clwwlknonel  30185  frgrncvvdeqlem9  30397  frgr2wwlkeqm  30421  frgrreggt1  30483  frgrreg  30484  pjhthmo  31393  spansncvi  31743  nmcexi  32117  cnlnssadj  32171  leopmuli  32224  elpjrn  32281  mdsl0  32401  sumdmdii  32506  fmptcof2  32750  suppss3  32816  lmxrge0  34117  bnj594  35075  bnj849  35088  noinfepfnregs  35297  subgrwlk  35335  erdszelem7  35400  sconnpi1  35442  cvmsval  35469  cvmopnlem  35481  cvmfolem  35482  cvmliftmolem2  35485  cvmlift2lem10  35515  cvmlift2lem12  35517  cvmlift3lem5  35526  cvmlift3lem8  35529  satfv0  35561  satfv1  35566  satfvsucsuc  35568  satffunlem1lem2  35606  satffunlem2lem2  35609  linethru  36356  opnrebl2  36524  neibastop2lem  36563  neibastop2  36564  bj-cbv3ta  37106  cgsex2gd  37464  isinf2  37732  phpreu  37936  finixpnum  37937  lindsadd  37945  matunitlindflem1  37948  ptrecube  37952  poimirlem26  37978  poimirlem27  37979  poimirlem31  37983  poimir  37985  heicant  37987  voliunnfl  37996  volsupnfl  37997  itg2addnclem  38003  unirep  38046  sdclem2  38074  istotbnd3  38103  ssbnd  38120  eldisjlem19  39245  lshpdisj  39444  lsatn0  39456  lsat0cv  39490  cvrletrN  39730  cvrval4N  39871  lncvrelatN  40238  paddasslem14  40290  paddasslem15  40291  paddasslem16  40292  pmapjoin  40309  dihglblem2N  41751  dochvalr  41814  eqresfnbd  42684  sn-sup2  42947  prjspner1  43070  flt4lem7  43103  incssnn0  43154  eldioph4b  43254  diophren  43256  fphpdo  43260  rencldnfilem  43263  pellexlem5  43276  pell1234qrne0  43296  pell1234qrmulcl  43298  pell14qrgt0  43302  pell1234qrdich  43304  pell14qrdich  43312  pell1qrge1  43313  pell1qrgap  43317  pellfundre  43324  pellfundlb  43327  dvdsacongtr  43427  jm2.19lem4  43435  aomclem4  43500  hbtlem2  43567  hbtlem4  43569  hbtlem6  43572  cantnfresb  43767  dflim5  43772  tfsconcatrn  43785  tfsconcatrev  43791  naddwordnexlem4  43844  safesnsupfiss  43857  harval3  43980  clcnvlem  44065  ordpss  44892  relpfrlem  45395  cfsetsnfsetfo  47505  euoreqb  47554  2reu8i  47558  sprsymrelf1lem  47948  sprsymrelfolem2  47950  reupr  47979  fmtnofac2lem  48028  opoeALTV  48156  opeoALTV  48157  fpprwpprb  48213  gboge9  48237  clnbgrel  48301  grimco  48362  uhgrimedgi  48363  isuspgrim  48369  cycldlenngric  48401  uhgrimisgrgric  48404  clnbgrgrimlem  48406  clnbgrgrim  48407  grtriprop  48414  stgrusgra  48432  grlimedgclnbgr  48468  grlimprclnbgrvtx  48472  grlimgredgex  48473  grlictr  48488  gpgedg2iv  48540  gpgcubic  48552  gpg5nbgr3star  48554  pgnbgreunbgrlem2  48590  pgnbgreunbgrlem5  48596  ellcoellss  48908  nn0sumshdiglem1  49094  itschlc0xyqsol  49240  itsclc0  49244  opnneilv  49381