Theorem expimpd 454

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ornld  1060  3impia  1117  ralrimdva  3154  disjiun  5134  reusv3  5402  euotd  5512  swopo  5598  sotr3  5626  wereu2  5672  poirr2  6122  sossfld  6182  reuop  6289  frpomin  6338  oneqmini  6413  suctr  6447  elpreima  7056  fmptco  7123  isofrlem  7333  onmindif2  7791  frxp  8108  fnse  8115  suppss  8175  suppssOLD  8176  tposfo2  8230  wfr3g  8303  tz7.48-2  8438  omeulem1  8578  omeu  8581  nnaordex  8634  eldifsucnn  8659  pssnn  9164  onomeneq  9224  pssnnOLD  9261  fodomfib  9322  dffi3  9422  supmo  9443  supnub  9453  infglb  9481  infnlb  9483  infmo  9486  infsupprpr  9495  cantnfle  9662  cantnflem1  9680  epfrs  9722  frr3g  9747  updjud  9925  alephord2i  10068  cardinfima  10088  aceq3lem  10111  dfac2b  10121  dfac12lem2  10135  axdc2lem  10439  ttukeylem6  10505  alephval2  10563  fpwwe2lem11  10632  fpwwe2lem12  10633  prlem934  11024  reclem4pr  11041  suplem1pr  11043  letr  11304  sup2  12166  uzind  12650  ledivge1le  13041  xrletr  13133  xltnegi  13191  xlemul1a  13263  ixxssixx  13334  difreicc  13457  flval3  13776  fsequb  13936  seqf1olem1  14003  expnegz  14058  hash2prd  14432  ccatrcl1  14540  relexprelg  14981  shftlem  15011  rexuzre  15295  cau3lem  15297  caubnd2  15300  caubnd  15301  climrlim2  15487  climuni  15492  2clim  15512  o1co  15526  rlimno1  15596  climbdd  15614  caurcvg  15619  summolem2  15658  summo  15659  zsum  15660  fsumf1o  15665  fsumss  15667  fsumcl2lem  15673  fsumadd  15682  fsummulc2  15726  fsumconst  15732  fsumrelem  15749  prodmolem2  15875  prodmo  15876  zprod  15877  fprodf1o  15886  fprodss  15888  fprodcl2lem  15890  fprodmul  15900  fproddiv  15901  fprodconst  15918  fprodn0  15919  dfgcd2  16484  lcmfunsnlem2  16573  coprmproddvdslem  16595  cncongrprm  16661  prmpwdvds  16833  infpnlem1  16839  1arith  16856  vdwapun  16903  vdwlem11  16920  vdwnnlem2  16925  ramz  16954  ramcl  16958  prmlem0  17035  firest  17374  catpropd  17649  initoid  17947  termoid  17948  initoeu2lem1  17960  pltnle  18287  pltletr  18292  pospo  18294  psss  18529  isgrpid2  18857  f1omvdco2  19310  pgpfi  19467  frgpnabllem1  19735  gsumval3eu  19766  gsumzres  19771  gsumzcl2  19772  gsumzf1o  19774  gsumzaddlem  19783  gsumconst  19796  gsumzmhm  19799  gsumzoppg  19806  ablfaclem3  19951  dvdsrtr  20174  dvdsrmul1  20175  unitgrp  20189  lspsolvlem  20747  domnmuln0  20906  gsumfsum  21004  obslbs  21276  gsummoncoe1  21819  pf1ind  21865  dmatscmcl  21996  scmatmulcl  22011  smatvscl  22017  mdetdiaglem  22091  cpmatinvcl  22210  mp2pm2mplem4  22302  cpmadugsumlemF  22369  eltg3  22456  tgidm  22474  neindisj  22612  tgrest  22654  restcld  22667  tgcn  22747  lmcnp  22799  iunconnlem  22922  2ndcredom  22945  2ndc1stc  22946  1stcrest  22948  2ndcrest  22949  2ndcdisj  22951  nllyrest  22981  nllyidm  22984  lfinpfin  23019  locfincmp  23021  ptpjpre1  23066  ptuni2  23071  ptbasin  23072  ptbasfi  23076  txbasval  23101  ptpjopn  23107  ptclsg  23110  dfac14lem  23112  xkoccn  23114  txcnp  23115  ptcnplem  23116  ptcnp  23117  txtube  23135  txcmplem1  23136  txcmplem2  23137  tx2ndc  23146  txkgen  23147  xkoco1cn  23152  xkoco2cn  23153  xkococnlem  23154  xkococn  23155  xkoinjcn  23182  qtoprest  23212  kqsat  23226  kqcldsat  23228  isfild  23353  fbunfip  23364  fgabs  23374  filconn  23378  fbasrn  23379  filufint  23415  elfm2  23443  elfm3  23445  fmfnfm  23453  hausflimi  23475  cnpflfi  23494  ptcmplem2  23548  tmdgsum2  23591  cldsubg  23606  qustgpopn  23615  ustfilxp  23708  bldisj  23895  xbln0  23911  blssps  23921  blss  23922  blssexps  23923  blssex  23924  blcls  24006  metcnp3  24040  icccmplem2  24330  cnheibor  24462  iscau4  24787  cmssmscld  24858  ovolshftlem2  25018  ovolicc2lem5  25029  dyadmax  25106  mbfi1fseqlem4  25227  mbfi1flimlem  25231  lhop1lem  25521  dvfsumrlim  25539  aalioulem3  25838  ulmcn  25902  radcnvlt1  25921  pilem2  25955  efopn  26157  cxpeq0  26177  cxpmul2z  26190  cxpcn3lem  26244  xrlimcnp  26462  vmappw  26609  fsumvma  26705  dchrptlem1  26756  lgsqr  26843  lgsdchrval  26846  2lgslem3  26896  2sqlem6  26915  2sqlem7  26916  2sqreultlem  26939  2sqreunnltlem  26942  pntlem3  27101  pntleml  27103  sltval2  27148  nosupno  27195  nosupbnd1lem5  27204  noinfno  27210  sletr  27250  madebdayim  27371  sltlpss  27390  negsid  27504  brbtwn  28146  brcgr  28147  axcontlem8  28218  nbumgrvtx  28592  cusgrfilem2  28702  1loopgrnb0  28748  uspgr2wlkeq  28892  wlklenvclwlk  28901  upgrwlkdvdelem  28982  uspgrn2crct  29051  0enwwlksnge1  29107  usgr2wspthons3  29207  clwwlkccatlem  29231  clwlkclwwlkf  29250  clwwlknonel  29337  frgrncvvdeqlem9  29549  frgr2wwlkeqm  29573  frgrreggt1  29635  frgrreg  29636  pjhthmo  30542  spansncvi  30892  nmcexi  31266  cnlnssadj  31320  leopmuli  31373  elpjrn  31430  mdsl0  31550  sumdmdii  31655  fmptcof2  31869  suppss3  31936  lmxrge0  32920  bnj594  33911  bnj849  33924  subgrwlk  34111  erdszelem7  34176  sconnpi1  34218  cvmsval  34245  cvmopnlem  34257  cvmfolem  34258  cvmliftmolem2  34261  cvmlift2lem10  34291  cvmlift2lem12  34293  cvmlift3lem5  34302  cvmlift3lem8  34305  satfv0  34337  satfv1  34342  satfvsucsuc  34344  satffunlem1lem2  34382  satffunlem2lem2  34385  linethru  35113  mpomulcn  35150  opnrebl2  35194  neibastop2lem  35233  neibastop2  35234  bj-cbv3ta  35652  isinf2  36274  phpreu  36460  finixpnum  36461  lindsadd  36469  matunitlindflem1  36472  ptrecube  36476  poimirlem26  36502  poimirlem27  36503  poimirlem31  36507  poimir  36509  heicant  36511  voliunnfl  36520  volsupnfl  36521  itg2addnclem  36527  unirep  36570  sdclem2  36598  istotbnd3  36627  ssbnd  36644  eldisjlem19  37668  lshpdisj  37845  lsatn0  37857  lsat0cv  37891  cvrletrN  38131  cvrval4N  38273  lncvrelatN  38640  paddasslem14  38692  paddasslem15  38693  paddasslem16  38694  pmapjoin  38711  dihglblem2N  40153  dochvalr  40216  eqresfnbd  41051  sn-negex12  41285  sn-sup2  41338  prjspner1  41364  flt4lem7  41397  incssnn0  41434  eldioph4b  41534  diophren  41536  fphpdo  41540  rencldnfilem  41543  pellexlem5  41556  pell1234qrne0  41576  pell1234qrmulcl  41578  pell14qrgt0  41582  pell1234qrdich  41584  pell14qrdich  41592  pell1qrge1  41593  pell1qrgap  41597  pellfundre  41604  pellfundlb  41607  dvdsacongtr  41708  jm2.19lem4  41716  aomclem4  41784  hbtlem2  41851  hbtlem4  41853  hbtlem6  41856  cantnfresb  42059  dflim5  42064  tfsconcatrn  42077  tfsconcatrev  42083  naddwordnexlem4  42137  safesnsupfiss  42151  harval3  42274  clcnvlem  42359  ordpss  43195  cfsetsnfsetfo  45756  euoreqb  45803  2reu8i  45807  sprsymrelf1lem  46145  sprsymrelfolem2  46147  reupr  46176  fmtnofac2lem  46222  opoeALTV  46337  opeoALTV  46338  fpprwpprb  46394  gboge9  46418  nzerooringczr  46923  ellcoellss  47069  nn0sumshdiglem1  47260  itschlc0xyqsol  47406  itsclc0  47410  opnneilv  47494