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  1117  ralrimdva  3160  disjiun  5154  reusv3  5423  euotd  5532  swopo  5619  sotr3  5648  wereu2  5697  poirr2  6156  sossfld  6217  reuop  6324  frpomin  6372  oneqmini  6447  suctr  6481  elpreima  7091  fmptco  7163  isofrlem  7376  onmindif2  7843  mptcnfimad  8027  frxp  8167  fnse  8174  suppss  8235  tposfo2  8290  wfr3g  8363  tz7.48-2  8498  omeulem1  8638  omeu  8641  nnaordex  8694  eldifsucnn  8720  pssnn  9234  onomeneq  9291  fodomfib  9397  fodomfibOLD  9399  dffi3  9500  supmo  9521  supnub  9531  infglb  9559  infnlb  9561  infmo  9564  infsupprpr  9573  cantnfle  9740  cantnflem1  9758  epfrs  9800  frr3g  9825  updjud  10003  alephord2i  10146  cardinfima  10166  aceq3lem  10189  dfac2b  10200  dfac12lem2  10214  axdc2lem  10517  ttukeylem6  10583  alephval2  10641  fpwwe2lem11  10710  fpwwe2lem12  10711  prlem934  11102  reclem4pr  11119  suplem1pr  11121  letr  11384  sup2  12251  uzind  12735  ledivge1le  13128  xrletr  13220  xltnegi  13278  xlemul1a  13350  ixxssixx  13421  difreicc  13544  flval3  13866  fsequb  14026  seqf1olem1  14092  expnegz  14147  hash2prd  14524  ccatrcl1  14642  relexprelg  15087  shftlem  15117  rexuzre  15401  cau3lem  15403  caubnd2  15406  caubnd  15407  climrlim2  15593  climuni  15598  2clim  15618  o1co  15632  rlimno1  15702  climbdd  15720  caurcvg  15725  summolem2  15764  summo  15765  zsum  15766  fsumf1o  15771  fsumss  15773  fsumcl2lem  15779  fsumadd  15788  fsummulc2  15832  fsumconst  15838  fsumrelem  15855  prodmolem2  15983  prodmo  15984  zprod  15985  fprodf1o  15994  fprodss  15996  fprodcl2lem  15998  fprodmul  16008  fproddiv  16009  fprodconst  16026  fprodn0  16027  dfgcd2  16593  lcmfunsnlem2  16687  coprmproddvdslem  16709  cncongrprm  16776  prmpwdvds  16951  infpnlem1  16957  1arith  16974  vdwapun  17021  vdwlem11  17038  vdwnnlem2  17043  ramz  17072  ramcl  17076  prmlem0  17153  firest  17492  catpropd  17767  initoid  18068  termoid  18069  initoeu2lem1  18081  pltnle  18408  pltletr  18413  pospo  18415  psss  18650  isgrpid2  19016  f1omvdco2  19490  pgpfi  19647  frgpnabllem1  19915  gsumval3eu  19946  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  gsumzoppg  19986  ablfaclem3  20131  dvdsrtr  20394  dvdsrmul1  20395  unitgrp  20409  domnmuln0  20731  lspsolvlem  21167  gsumfsum  21475  nzerooringczr  21514  obslbs  21773  gsummoncoe1  22333  pf1ind  22380  dmatscmcl  22530  scmatmulcl  22545  smatvscl  22551  mdetdiaglem  22625  cpmatinvcl  22744  mp2pm2mplem4  22836  cpmadugsumlemF  22903  eltg3  22990  tgidm  23008  neindisj  23146  tgrest  23188  restcld  23201  tgcn  23281  lmcnp  23333  iunconnlem  23456  2ndcredom  23479  2ndc1stc  23480  1stcrest  23482  2ndcrest  23483  2ndcdisj  23485  nllyrest  23515  nllyidm  23518  lfinpfin  23553  locfincmp  23555  ptpjpre1  23600  ptuni2  23605  ptbasin  23606  ptbasfi  23610  txbasval  23635  ptpjopn  23641  ptclsg  23644  dfac14lem  23646  xkoccn  23648  txcnp  23649  ptcnplem  23650  ptcnp  23651  txtube  23669  txcmplem1  23670  txcmplem2  23671  tx2ndc  23680  txkgen  23681  xkoco1cn  23686  xkoco2cn  23687  xkococnlem  23688  xkococn  23689  xkoinjcn  23716  qtoprest  23746  kqsat  23760  kqcldsat  23762  isfild  23887  fbunfip  23898  fgabs  23908  filconn  23912  fbasrn  23913  filufint  23949  elfm2  23977  elfm3  23979  fmfnfm  23987  hausflimi  24009  cnpflfi  24028  ptcmplem2  24082  tmdgsum2  24125  cldsubg  24140  qustgpopn  24149  ustfilxp  24242  bldisj  24429  xbln0  24445  blssps  24455  blss  24456  blssexps  24457  blssex  24458  blcls  24540  metcnp3  24574  icccmplem2  24864  mpomulcn  24910  cnheibor  25006  iscau4  25332  cmssmscld  25403  ovolshftlem2  25564  ovolicc2lem5  25575  dyadmax  25652  mbfi1fseqlem4  25773  mbfi1flimlem  25777  lhop1lem  26072  dvfsumrlim  26092  aalioulem3  26394  ulmcn  26460  radcnvlt1  26479  pilem2  26514  efopn  26718  cxpeq0  26738  cxpmul2z  26751  cxpcn3lem  26808  xrlimcnp  27029  vmappw  27177  fsumvma  27275  dchrptlem1  27326  lgsqr  27413  lgsdchrval  27416  2lgslem3  27466  2sqlem6  27485  2sqlem7  27486  2sqreultlem  27509  2sqreunnltlem  27512  pntlem3  27671  pntleml  27673  sltval2  27719  nosupno  27766  nosupbnd1lem5  27775  noinfno  27781  sletr  27821  madebdayim  27944  sltlpss  27963  negsid  28091  noseqinds  28317  brbtwn  28932  brcgr  28933  axcontlem8  29004  nbumgrvtx  29381  cusgrfilem2  29492  1loopgrnb0  29538  uspgr2wlkeq  29682  wlklenvclwlk  29691  upgrwlkdvdelem  29772  uspgrn2crct  29841  0enwwlksnge1  29897  usgr2wspthons3  29997  clwwlkccatlem  30021  clwlkclwwlkf  30040  clwwlknonel  30127  frgrncvvdeqlem9  30339  frgr2wwlkeqm  30363  frgrreggt1  30425  frgrreg  30426  pjhthmo  31334  spansncvi  31684  nmcexi  32058  cnlnssadj  32112  leopmuli  32165  elpjrn  32222  mdsl0  32342  sumdmdii  32447  fmptcof2  32675  suppss3  32738  lmxrge0  33898  bnj594  34888  bnj849  34901  subgrwlk  35100  erdszelem7  35165  sconnpi1  35207  cvmsval  35234  cvmopnlem  35246  cvmfolem  35247  cvmliftmolem2  35250  cvmlift2lem10  35280  cvmlift2lem12  35282  cvmlift3lem5  35291  cvmlift3lem8  35294  satfv0  35326  satfv1  35331  satfvsucsuc  35333  satffunlem1lem2  35371  satffunlem2lem2  35374  linethru  36117  opnrebl2  36287  neibastop2lem  36326  neibastop2  36327  bj-cbv3ta  36752  isinf2  37371  phpreu  37564  finixpnum  37565  lindsadd  37573  matunitlindflem1  37576  ptrecube  37580  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  poimir  37613  heicant  37615  voliunnfl  37624  volsupnfl  37625  itg2addnclem  37631  unirep  37674  sdclem2  37702  istotbnd3  37731  ssbnd  37748  eldisjlem19  38766  lshpdisj  38943  lsatn0  38955  lsat0cv  38989  cvrletrN  39229  cvrval4N  39371  lncvrelatN  39738  paddasslem14  39790  paddasslem15  39791  paddasslem16  39792  pmapjoin  39809  dihglblem2N  41251  dochvalr  41314  eqresfnbd  42227  sn-sup2  42447  prjspner1  42581  flt4lem7  42614  incssnn0  42667  eldioph4b  42767  diophren  42769  fphpdo  42773  rencldnfilem  42776  pellexlem5  42789  pell1234qrne0  42809  pell1234qrmulcl  42811  pell14qrgt0  42815  pell1234qrdich  42817  pell14qrdich  42825  pell1qrge1  42826  pell1qrgap  42830  pellfundre  42837  pellfundlb  42840  dvdsacongtr  42941  jm2.19lem4  42949  aomclem4  43014  hbtlem2  43081  hbtlem4  43083  hbtlem6  43086  cantnfresb  43286  dflim5  43291  tfsconcatrn  43304  tfsconcatrev  43310  naddwordnexlem4  43363  safesnsupfiss  43377  harval3  43500  clcnvlem  43585  ordpss  44420  cfsetsnfsetfo  46975  euoreqb  47024  2reu8i  47028  sprsymrelf1lem  47365  sprsymrelfolem2  47367  reupr  47396  fmtnofac2lem  47442  opoeALTV  47557  opeoALTV  47558  fpprwpprb  47614  gboge9  47638  clnbgrel  47701  isuspgrim  47759  grimco  47764  uhgrimisgrgric  47783  clnbgrgrimlem  47785  clnbgrgrim  47786  grtriprop  47792  grlictr  47832  ellcoellss  48164  nn0sumshdiglem1  48355  itschlc0xyqsol  48501  itsclc0  48505  opnneilv  48588