Theorem expimpd 458

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 417	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 415	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ornld  1075  3impia  1133  ralrimdva  3165  disjiun  5093  reusv3  5367  euotd  5487  swopo  5571  sotr3  5601  wereu2  5649  poirr2  6115  sossfld  6176  reuop  6284  frpomin  6331  oneqmini  6403  suctr  6438  elpreima  7043  fmptco  7115  isofrlem  7328  onmindif2  7794  resf1extb  7919  mptcnfimad  7971  frxp  8110  fnse  8117  suppss  8178  tposfo2  8233  wfr3g  8304  tz7.48-2  8417  omeulem1  8555  omeu  8558  nnaordex  8612  eldifsucnn  8638  pssnn  9141  onomeneq  9186  fodomfib  9276  dffi3  9379  supmo  9400  supnub  9410  infglb  9439  infnlb  9441  infmo  9445  infsupprpr  9454  cantnfle  9628  cantnflem1  9646  epfrs  9688  frr3g  9716  updjud  9908  alephord2i  10049  cardinfima  10069  aceq3lem  10092  dfac2b  10102  dfac12lem2  10116  axdc2lem  10420  ttukeylem6  10486  alephval2  10545  fpwwe2lem11  10614  fpwwe2lem12  10615  prlem934  11006  reclem4pr  11023  suplem1pr  11025  letr  11292  sup2  12162  uzind  12679  ledivge1le  13080  xrletr  13174  xltnegi  13233  xlemul1a  13305  ixxssixx  13377  difreicc  13502  flval3  13839  fsequb  14002  seqf1olem1  14068  expnegz  14123  hash2prd  14502  ccatrcl1  14622  relexprelg  15065  shftlem  15095  rexuzre  15394  cau3lem  15396  caubnd2  15399  caubnd  15400  climrlim2  15588  climuni  15593  2clim  15613  o1co  15627  rlimno1  15695  climbdd  15713  caurcvg  15718  summolem2  15757  summo  15758  zsum  15759  fsumf1o  15764  fsumss  15766  fsumcl2lem  15772  fsumadd  15781  fsummulc2  15825  fsumconst  15831  fsumrelem  15849  prodmolem2  15979  prodmo  15980  zprod  15981  fprodf1o  15990  fprodss  15992  fprodcl2lem  15994  fprodmul  16004  fproddiv  16005  fprodconst  16022  fprodn0  16023  dfgcd2  16594  lcmfunsnlem2  16688  coprmproddvdslem  16710  cncongrprm  16778  prmpwdvds  16954  infpnlem1  16960  1arith  16977  vdwapun  17024  vdwlem11  17041  vdwnnlem2  17046  ramz  17075  ramcl  17079  prmlem0  17155  firest  17475  catpropd  17755  initoid  18048  termoid  18049  initoeu2lem1  18061  pltnle  18382  pltletr  18387  pospo  18389  psss  18626  isgrpid2  19033  f1omvdco2  19509  pgpfi  19666  frgpnabllem1  19934  gsumval3eu  19965  gsumzres  19970  gsumzcl2  19971  gsumzf1o  19973  gsumzaddlem  19982  gsumconst  19995  gsumzmhm  19998  gsumzoppg  20005  ablfaclem3  20150  dvdsrtr  20441  dvdsrmul1  20442  unitgrp  20456  domnmuln0  20785  lspsolvlem  21235  gsumfsum  21544  nzerooringczr  21590  obslbs  21840  gsummoncoe1  22429  pf1ind  22476  dmatscmcl  22621  scmatmulcl  22636  smatvscl  22642  mdetdiaglem  22716  cpmatinvcl  22835  mp2pm2mplem4  22927  cpmadugsumlemF  22994  eltg3  23080  tgidm  23098  neindisj  23235  tgrest  23277  restcld  23290  tgcn  23370  lmcnp  23422  iunconnlem  23545  2ndcredom  23568  2ndc1stc  23569  1stcrest  23571  2ndcrest  23572  2ndcdisj  23574  nllyrest  23604  nllyidm  23607  lfinpfin  23642  locfincmp  23644  ptpjpre1  23689  ptuni2  23694  ptbasin  23695  ptbasfi  23699  txbasval  23724  ptpjopn  23730  ptclsg  23733  dfac14lem  23735  xkoccn  23737  txcnp  23738  ptcnplem  23739  ptcnp  23740  txtube  23758  txcmplem1  23759  txcmplem2  23760  tx2ndc  23769  txkgen  23770  xkoco1cn  23775  xkoco2cn  23776  xkococnlem  23777  xkococn  23778  xkoinjcn  23805  qtoprest  23835  kqsat  23849  kqcldsat  23851  isfild  23976  fbunfip  23987  fgabs  23997  filconn  24001  fbasrn  24002  filufint  24038  elfm2  24066  elfm3  24068  fmfnfm  24076  hausflimi  24098  cnpflfi  24117  ptcmplem2  24171  tmdgsum2  24214  cldsubg  24229  qustgpopn  24238  ustfilxp  24331  bldisj  24516  xbln0  24532  blssps  24542  blss  24543  blssexps  24544  blssex  24545  blcls  24624  metcnp3  24658  icccmplem2  24942  mpomulcn  24987  cnheibor  25075  iscau4  25399  cmssmscld  25470  ovolshftlem2  25630  ovolicc2lem5  25641  dyadmax  25718  mbfi1fseqlem4  25838  mbfi1flimlem  25842  lhop1lem  26133  dvfsumrlim  26151  aalioulem3  26456  ulmcn  26520  radcnvlt1  26539  pilem2  26573  efopn  26781  cxpeq0  26801  cxpmul2z  26814  cxpcn3lem  26870  xrlimcnp  27091  vmappw  27238  fsumvma  27335  dchrptlem1  27386  lgsqr  27473  lgsdchrval  27476  2lgslem3  27526  2sqlem6  27545  2sqlem7  27546  2sqreultlem  27569  2sqreunnltlem  27572  pntlem3  27731  pntleml  27733  ltsval2  27778  nosupno  27825  nosupbnd1lem5  27834  noinfno  27840  lestr  27884  madebdayim  28039  ltslpss  28059  negsid  28192  noseqinds  28444  brbtwn  29158  brcgr  29159  axcontlem8  29230  nbumgrvtx  29605  cusgrfilem2  29715  1loopgrnb0  29761  uspgr2wlkeq  29904  wlklenvclwlk  29912  upgrwlkdvdelem  29994  uspgrn2crct  30066  0enwwlksnge1  30122  usgr2wspthons3  30225  clwwlkccatlem  30249  clwlkclwwlkf  30268  clwwlknonel  30355  frgrncvvdeqlem9  30567  frgr2wwlkeqm  30591  frgrreggt1  30653  frgrreg  30654  pjhthmo  31563  spansncvi  31913  nmcexi  32287  cnlnssadj  32341  leopmuli  32394  elpjrn  32451  mdsl0  32571  sumdmdii  32676  fmptcof2  32914  suppss3  32980  lmxrge0  34259  bnj594  35217  bnj849  35230  noinfepfnregs  35440  subgrwlk  35495  erdszelem7  35560  sconnpi1  35602  cvmsval  35629  cvmopnlem  35641  cvmfolem  35642  cvmliftmolem2  35645  cvmlift2lem10  35675  cvmlift2lem12  35677  cvmlift3lem5  35686  cvmlift3lem8  35689  satfv0  35721  satfv1  35726  satfvsucsuc  35728  satffunlem1lem2  35766  satffunlem2lem2  35769  linethru  36516  opnrebl2  36694  neibastop2lem  36733  neibastop2  36734  bj-cbv3ta  37283  cgsex2gd  37641  isinf2  37911  phpreu  38115  finixpnum  38116  lindsadd  38124  matunitlindflem1  38127  ptrecube  38131  poimirlem26  38157  poimirlem27  38158  poimirlem31  38162  poimir  38164  heicant  38166  voliunnfl  38175  volsupnfl  38176  itg2addnclem  38182  unirep  38225  sdclem2  38253  istotbnd3  38282  ssbnd  38299  eldisjlem19  39424  lshpdisj  39623  lsatn0  39635  lsat0cv  39669  cvrletrN  39909  cvrval4N  40050  lncvrelatN  40417  paddasslem14  40469  paddasslem15  40470  paddasslem16  40471  pmapjoin  40488  dihglblem2N  41930  dochvalr  41993  eqresfnbd  42863  sn-sup2  43125  prjspner1  43220  flt4lem7  43253  incssnn0  43304  eldioph4b  43400  diophren  43402  fphpdo  43406  rencldnfilem  43409  pellexlem5  43422  pell1234qrne0  43442  pell1234qrmulcl  43444  pell14qrgt0  43448  pell1234qrdich  43450  pell14qrdich  43458  pell1qrge1  43459  pell1qrgap  43463  pellfundre  43470  pellfundlb  43473  dvdsacongtr  43573  jm2.19lem4  43581  aomclem4  43646  hbtlem2  43713  hbtlem4  43715  hbtlem6  43718  cantnfresb  43913  dflim5  43918  tfsconcatrn  43931  tfsconcatrev  43937  naddwordnexlem4  43990  safesnsupfiss  44003  harval3  44126  clcnvlem  44211  ordpss  45024  relpfrlem  45527  cfsetsnfsetfo  47652  euoreqb  47701  2reu8i  47705  sprsymrelf1lem  48095  sprsymrelfolem2  48097  reupr  48126  fmtnofac2lem  48175  opoeALTV  48303  opeoALTV  48304  fpprwpprb  48360  gboge9  48384  clnbgrel  48448  grimco  48509  uhgrimedgi  48510  isuspgrim  48516  cycldlenngric  48548  uhgrimisgrgric  48551  clnbgrgrimlem  48553  clnbgrgrim  48554  grtriprop  48561  stgrusgra  48579  grlimedgclnbgr  48615  grlimprclnbgrvtx  48619  grlimgredgex  48620  grlictr  48635  gpgedg2iv  48687  gpgcubic  48699  gpg5nbgr3star  48701  pgnbgreunbgrlem2  48737  pgnbgreunbgrlem5  48743  ellcoellss  49066  nn0sumshdiglem1  49252  itschlc0xyqsol  49398  itsclc0  49402  opnneilv  49538