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  1061  3impia  1116  ralrimdva  3152  disjiun  5136  reusv3  5411  euotd  5523  swopo  5608  sotr3  5637  wereu2  5686  poirr2  6147  sossfld  6208  reuop  6315  frpomin  6363  oneqmini  6438  suctr  6472  elpreima  7078  fmptco  7149  isofrlem  7360  onmindif2  7827  mptcnfimad  8010  frxp  8150  fnse  8157  suppss  8218  tposfo2  8273  wfr3g  8346  tz7.48-2  8481  omeulem1  8619  omeu  8622  nnaordex  8675  eldifsucnn  8701  pssnn  9207  onomeneq  9263  fodomfib  9367  fodomfibOLD  9369  dffi3  9469  supmo  9490  supnub  9500  infglb  9528  infnlb  9530  infmo  9533  infsupprpr  9542  cantnfle  9709  cantnflem1  9727  epfrs  9769  frr3g  9794  updjud  9972  alephord2i  10115  cardinfima  10135  aceq3lem  10158  dfac2b  10169  dfac12lem2  10183  axdc2lem  10486  ttukeylem6  10552  alephval2  10610  fpwwe2lem11  10679  fpwwe2lem12  10680  prlem934  11071  reclem4pr  11088  suplem1pr  11090  letr  11353  sup2  12222  uzind  12708  ledivge1le  13104  xrletr  13197  xltnegi  13255  xlemul1a  13327  ixxssixx  13398  difreicc  13521  flval3  13852  fsequb  14013  seqf1olem1  14079  expnegz  14134  hash2prd  14511  ccatrcl1  14629  relexprelg  15074  shftlem  15104  rexuzre  15388  cau3lem  15390  caubnd2  15393  caubnd  15394  climrlim2  15580  climuni  15585  2clim  15605  o1co  15619  rlimno1  15687  climbdd  15705  caurcvg  15710  summolem2  15749  summo  15750  zsum  15751  fsumf1o  15756  fsumss  15758  fsumcl2lem  15764  fsumadd  15773  fsummulc2  15817  fsumconst  15823  fsumrelem  15840  prodmolem2  15968  prodmo  15969  zprod  15970  fprodf1o  15979  fprodss  15981  fprodcl2lem  15983  fprodmul  15993  fproddiv  15994  fprodconst  16011  fprodn0  16012  dfgcd2  16580  lcmfunsnlem2  16674  coprmproddvdslem  16696  cncongrprm  16763  prmpwdvds  16938  infpnlem1  16944  1arith  16961  vdwapun  17008  vdwlem11  17025  vdwnnlem2  17030  ramz  17059  ramcl  17063  prmlem0  17140  firest  17479  catpropd  17754  initoid  18055  termoid  18056  initoeu2lem1  18068  pltnle  18396  pltletr  18401  pospo  18403  psss  18638  isgrpid2  19007  f1omvdco2  19481  pgpfi  19638  frgpnabllem1  19906  gsumval3eu  19937  gsumzres  19942  gsumzcl2  19943  gsumzf1o  19945  gsumzaddlem  19954  gsumconst  19967  gsumzmhm  19970  gsumzoppg  19977  ablfaclem3  20122  dvdsrtr  20385  dvdsrmul1  20386  unitgrp  20400  domnmuln0  20726  lspsolvlem  21162  gsumfsum  21470  nzerooringczr  21509  obslbs  21768  gsummoncoe1  22328  pf1ind  22375  dmatscmcl  22525  scmatmulcl  22540  smatvscl  22546  mdetdiaglem  22620  cpmatinvcl  22739  mp2pm2mplem4  22831  cpmadugsumlemF  22898  eltg3  22985  tgidm  23003  neindisj  23141  tgrest  23183  restcld  23196  tgcn  23276  lmcnp  23328  iunconnlem  23451  2ndcredom  23474  2ndc1stc  23475  1stcrest  23477  2ndcrest  23478  2ndcdisj  23480  nllyrest  23510  nllyidm  23513  lfinpfin  23548  locfincmp  23550  ptpjpre1  23595  ptuni2  23600  ptbasin  23601  ptbasfi  23605  txbasval  23630  ptpjopn  23636  ptclsg  23639  dfac14lem  23641  xkoccn  23643  txcnp  23644  ptcnplem  23645  ptcnp  23646  txtube  23664  txcmplem1  23665  txcmplem2  23666  tx2ndc  23675  txkgen  23676  xkoco1cn  23681  xkoco2cn  23682  xkococnlem  23683  xkococn  23684  xkoinjcn  23711  qtoprest  23741  kqsat  23755  kqcldsat  23757  isfild  23882  fbunfip  23893  fgabs  23903  filconn  23907  fbasrn  23908  filufint  23944  elfm2  23972  elfm3  23974  fmfnfm  23982  hausflimi  24004  cnpflfi  24023  ptcmplem2  24077  tmdgsum2  24120  cldsubg  24135  qustgpopn  24144  ustfilxp  24237  bldisj  24424  xbln0  24440  blssps  24450  blss  24451  blssexps  24452  blssex  24453  blcls  24535  metcnp3  24569  icccmplem2  24859  mpomulcn  24905  cnheibor  25001  iscau4  25327  cmssmscld  25398  ovolshftlem2  25559  ovolicc2lem5  25570  dyadmax  25647  mbfi1fseqlem4  25768  mbfi1flimlem  25772  lhop1lem  26067  dvfsumrlim  26087  aalioulem3  26391  ulmcn  26457  radcnvlt1  26476  pilem2  26511  efopn  26715  cxpeq0  26735  cxpmul2z  26748  cxpcn3lem  26805  xrlimcnp  27026  vmappw  27174  fsumvma  27272  dchrptlem1  27323  lgsqr  27410  lgsdchrval  27413  2lgslem3  27463  2sqlem6  27482  2sqlem7  27483  2sqreultlem  27506  2sqreunnltlem  27509  pntlem3  27668  pntleml  27670  sltval2  27716  nosupno  27763  nosupbnd1lem5  27772  noinfno  27778  sletr  27818  madebdayim  27941  sltlpss  27960  negsid  28088  noseqinds  28314  brbtwn  28929  brcgr  28930  axcontlem8  29001  nbumgrvtx  29378  cusgrfilem2  29489  1loopgrnb0  29535  uspgr2wlkeq  29679  wlklenvclwlk  29688  upgrwlkdvdelem  29769  uspgrn2crct  29838  0enwwlksnge1  29894  usgr2wspthons3  29994  clwwlkccatlem  30018  clwlkclwwlkf  30037  clwwlknonel  30124  frgrncvvdeqlem9  30336  frgr2wwlkeqm  30360  frgrreggt1  30422  frgrreg  30423  pjhthmo  31331  spansncvi  31681  nmcexi  32055  cnlnssadj  32109  leopmuli  32162  elpjrn  32219  mdsl0  32339  sumdmdii  32444  fmptcof2  32674  suppss3  32742  lmxrge0  33913  bnj594  34905  bnj849  34918  subgrwlk  35117  erdszelem7  35182  sconnpi1  35224  cvmsval  35251  cvmopnlem  35263  cvmfolem  35264  cvmliftmolem2  35267  cvmlift2lem10  35297  cvmlift2lem12  35299  cvmlift3lem5  35308  cvmlift3lem8  35311  satfv0  35343  satfv1  35348  satfvsucsuc  35350  satffunlem1lem2  35388  satffunlem2lem2  35391  linethru  36135  opnrebl2  36304  neibastop2lem  36343  neibastop2  36344  bj-cbv3ta  36769  isinf2  37388  phpreu  37591  finixpnum  37592  lindsadd  37600  matunitlindflem1  37603  ptrecube  37607  poimirlem26  37633  poimirlem27  37634  poimirlem31  37638  poimir  37640  heicant  37642  voliunnfl  37651  volsupnfl  37652  itg2addnclem  37658  unirep  37701  sdclem2  37729  istotbnd3  37758  ssbnd  37775  eldisjlem19  38792  lshpdisj  38969  lsatn0  38981  lsat0cv  39015  cvrletrN  39255  cvrval4N  39397  lncvrelatN  39764  paddasslem14  39816  paddasslem15  39817  paddasslem16  39818  pmapjoin  39835  dihglblem2N  41277  dochvalr  41340  eqresfnbd  42252  sn-sup2  42478  prjspner1  42613  flt4lem7  42646  incssnn0  42699  eldioph4b  42799  diophren  42801  fphpdo  42805  rencldnfilem  42808  pellexlem5  42821  pell1234qrne0  42841  pell1234qrmulcl  42843  pell14qrgt0  42847  pell1234qrdich  42849  pell14qrdich  42857  pell1qrge1  42858  pell1qrgap  42862  pellfundre  42869  pellfundlb  42872  dvdsacongtr  42973  jm2.19lem4  42981  aomclem4  43046  hbtlem2  43113  hbtlem4  43115  hbtlem6  43118  cantnfresb  43314  dflim5  43319  tfsconcatrn  43332  tfsconcatrev  43338  naddwordnexlem4  43391  safesnsupfiss  43405  harval3  43528  clcnvlem  43613  ordpss  44447  cfsetsnfsetfo  47010  euoreqb  47059  2reu8i  47063  sprsymrelf1lem  47416  sprsymrelfolem2  47418  reupr  47447  fmtnofac2lem  47493  opoeALTV  47608  opeoALTV  47609  fpprwpprb  47665  gboge9  47689  clnbgrel  47753  isuspgrim  47813  grimco  47818  uhgrimisgrgric  47837  clnbgrgrimlem  47839  clnbgrgrim  47840  grtriprop  47846  stgrusgra  47862  grlictr  47911  gpgcubic  47970  gpg5nbgr3star  47972  ellcoellss  48281  nn0sumshdiglem1  48471  itschlc0xyqsol  48617  itsclc0  48621  opnneilv  48705