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  1117  ralrimdva  3130  disjiun  5077  reusv3  5341  euotd  5451  swopo  5533  sotr3  5563  wereu2  5611  poirr2  6068  sossfld  6130  reuop  6236  frpomin  6283  oneqmini  6355  suctr  6390  elpreima  6986  fmptco  7057  isofrlem  7269  onmindif2  7735  resf1extb  7859  mptcnfimad  7913  frxp  8051  fnse  8058  suppss  8119  tposfo2  8174  wfr3g  8244  tz7.48-2  8356  omeulem1  8492  omeu  8495  nnaordex  8548  eldifsucnn  8574  pssnn  9073  onomeneq  9118  fodomfib  9208  fodomfibOLD  9210  dffi3  9310  supmo  9331  supnub  9341  infglb  9370  infnlb  9372  infmo  9376  infsupprpr  9385  cantnfle  9556  cantnflem1  9574  epfrs  9616  frr3g  9641  updjud  9819  alephord2i  9960  cardinfima  9980  aceq3lem  10003  dfac2b  10014  dfac12lem2  10028  axdc2lem  10331  ttukeylem6  10397  alephval2  10455  fpwwe2lem11  10524  fpwwe2lem12  10525  prlem934  10916  reclem4pr  10933  suplem1pr  10935  letr  11199  sup2  12070  uzind  12557  ledivge1le  12955  xrletr  13049  xltnegi  13107  xlemul1a  13179  ixxssixx  13251  difreicc  13376  flval3  13711  fsequb  13874  seqf1olem1  13940  expnegz  13995  hash2prd  14374  ccatrcl1  14494  relexprelg  14937  shftlem  14967  rexuzre  15252  cau3lem  15254  caubnd2  15257  caubnd  15258  climrlim2  15446  climuni  15451  2clim  15471  o1co  15485  rlimno1  15553  climbdd  15571  caurcvg  15576  summolem2  15615  summo  15616  zsum  15617  fsumf1o  15622  fsumss  15624  fsumcl2lem  15630  fsumadd  15639  fsummulc2  15683  fsumconst  15689  fsumrelem  15706  prodmolem2  15834  prodmo  15835  zprod  15836  fprodf1o  15845  fprodss  15847  fprodcl2lem  15849  fprodmul  15859  fproddiv  15860  fprodconst  15877  fprodn0  15878  dfgcd2  16449  lcmfunsnlem2  16543  coprmproddvdslem  16565  cncongrprm  16632  prmpwdvds  16808  infpnlem1  16814  1arith  16831  vdwapun  16878  vdwlem11  16895  vdwnnlem2  16900  ramz  16929  ramcl  16933  prmlem0  17009  firest  17328  catpropd  17607  initoid  17900  termoid  17901  initoeu2lem1  17913  pltnle  18234  pltletr  18239  pospo  18241  psss  18478  isgrpid2  18881  f1omvdco2  19353  pgpfi  19510  frgpnabllem1  19778  gsumval3eu  19809  gsumzres  19814  gsumzcl2  19815  gsumzf1o  19817  gsumzaddlem  19826  gsumconst  19839  gsumzmhm  19842  gsumzoppg  19849  ablfaclem3  19994  dvdsrtr  20279  dvdsrmul1  20280  unitgrp  20294  domnmuln0  20617  lspsolvlem  21072  gsumfsum  21364  nzerooringczr  21410  obslbs  21660  gsummoncoe1  22216  pf1ind  22263  dmatscmcl  22411  scmatmulcl  22426  smatvscl  22432  mdetdiaglem  22506  cpmatinvcl  22625  mp2pm2mplem4  22717  cpmadugsumlemF  22784  eltg3  22870  tgidm  22888  neindisj  23025  tgrest  23067  restcld  23080  tgcn  23160  lmcnp  23212  iunconnlem  23335  2ndcredom  23358  2ndc1stc  23359  1stcrest  23361  2ndcrest  23362  2ndcdisj  23364  nllyrest  23394  nllyidm  23397  lfinpfin  23432  locfincmp  23434  ptpjpre1  23479  ptuni2  23484  ptbasin  23485  ptbasfi  23489  txbasval  23514  ptpjopn  23520  ptclsg  23523  dfac14lem  23525  xkoccn  23527  txcnp  23528  ptcnplem  23529  ptcnp  23530  txtube  23548  txcmplem1  23549  txcmplem2  23550  tx2ndc  23559  txkgen  23560  xkoco1cn  23565  xkoco2cn  23566  xkococnlem  23567  xkococn  23568  xkoinjcn  23595  qtoprest  23625  kqsat  23639  kqcldsat  23641  isfild  23766  fbunfip  23777  fgabs  23787  filconn  23791  fbasrn  23792  filufint  23828  elfm2  23856  elfm3  23858  fmfnfm  23866  hausflimi  23888  cnpflfi  23907  ptcmplem2  23961  tmdgsum2  24004  cldsubg  24019  qustgpopn  24028  ustfilxp  24121  bldisj  24306  xbln0  24322  blssps  24332  blss  24333  blssexps  24334  blssex  24335  blcls  24414  metcnp3  24448  icccmplem2  24732  mpomulcn  24778  cnheibor  24874  iscau4  25199  cmssmscld  25270  ovolshftlem2  25431  ovolicc2lem5  25442  dyadmax  25519  mbfi1fseqlem4  25639  mbfi1flimlem  25643  lhop1lem  25938  dvfsumrlim  25958  aalioulem3  26262  ulmcn  26328  radcnvlt1  26347  pilem2  26382  efopn  26587  cxpeq0  26607  cxpmul2z  26620  cxpcn3lem  26677  xrlimcnp  26898  vmappw  27046  fsumvma  27144  dchrptlem1  27195  lgsqr  27282  lgsdchrval  27285  2lgslem3  27335  2sqlem6  27354  2sqlem7  27355  2sqreultlem  27378  2sqreunnltlem  27381  pntlem3  27540  pntleml  27542  sltval2  27588  nosupno  27635  nosupbnd1lem5  27644  noinfno  27650  sletr  27690  madebdayim  27826  sltlpss  27846  negsid  27976  noseqinds  28216  brbtwn  28870  brcgr  28871  axcontlem8  28942  nbumgrvtx  29317  cusgrfilem2  29428  1loopgrnb0  29474  uspgr2wlkeq  29617  wlklenvclwlk  29625  upgrwlkdvdelem  29707  uspgrn2crct  29779  0enwwlksnge1  29835  usgr2wspthons3  29935  clwwlkccatlem  29959  clwlkclwwlkf  29978  clwwlknonel  30065  frgrncvvdeqlem9  30277  frgr2wwlkeqm  30301  frgrreggt1  30363  frgrreg  30364  pjhthmo  31272  spansncvi  31622  nmcexi  31996  cnlnssadj  32050  leopmuli  32103  elpjrn  32160  mdsl0  32280  sumdmdii  32385  fmptcof2  32629  suppss3  32696  lmxrge0  33955  bnj594  34914  bnj849  34927  subgrwlk  35144  erdszelem7  35209  sconnpi1  35251  cvmsval  35278  cvmopnlem  35290  cvmfolem  35291  cvmliftmolem2  35294  cvmlift2lem10  35324  cvmlift2lem12  35326  cvmlift3lem5  35335  cvmlift3lem8  35338  satfv0  35370  satfv1  35375  satfvsucsuc  35377  satffunlem1lem2  35415  satffunlem2lem2  35418  linethru  36166  opnrebl2  36334  neibastop2lem  36373  neibastop2  36374  bj-cbv3ta  36799  isinf2  37418  phpreu  37623  finixpnum  37624  lindsadd  37632  matunitlindflem1  37635  ptrecube  37639  poimirlem26  37665  poimirlem27  37666  poimirlem31  37670  poimir  37672  heicant  37674  voliunnfl  37683  volsupnfl  37684  itg2addnclem  37690  unirep  37733  sdclem2  37761  istotbnd3  37790  ssbnd  37807  eldisjlem19  38827  lshpdisj  39005  lsatn0  39017  lsat0cv  39051  cvrletrN  39291  cvrval4N  39432  lncvrelatN  39799  paddasslem14  39851  paddasslem15  39852  paddasslem16  39853  pmapjoin  39870  dihglblem2N  41312  dochvalr  41375  eqresfnbd  42244  sn-sup2  42503  prjspner1  42638  flt4lem7  42671  incssnn0  42723  eldioph4b  42823  diophren  42825  fphpdo  42829  rencldnfilem  42832  pellexlem5  42845  pell1234qrne0  42865  pell1234qrmulcl  42867  pell14qrgt0  42871  pell1234qrdich  42873  pell14qrdich  42881  pell1qrge1  42882  pell1qrgap  42886  pellfundre  42893  pellfundlb  42896  dvdsacongtr  42996  jm2.19lem4  43004  aomclem4  43069  hbtlem2  43136  hbtlem4  43138  hbtlem6  43141  cantnfresb  43336  dflim5  43341  tfsconcatrn  43354  tfsconcatrev  43360  naddwordnexlem4  43413  safesnsupfiss  43427  harval3  43550  clcnvlem  43635  ordpss  44462  relpfrlem  44965  cfsetsnfsetfo  47070  euoreqb  47119  2reu8i  47123  sprsymrelf1lem  47501  sprsymrelfolem2  47503  reupr  47532  fmtnofac2lem  47578  opoeALTV  47693  opeoALTV  47694  fpprwpprb  47750  gboge9  47774  clnbgrel  47838  grimco  47899  uhgrimedgi  47900  isuspgrim  47906  cycldlenngric  47938  uhgrimisgrgric  47941  clnbgrgrimlem  47943  clnbgrgrim  47944  grtriprop  47951  stgrusgra  47969  grlimedgclnbgr  48005  grlimprclnbgrvtx  48009  grlimgredgex  48010  grlictr  48025  gpgedg2iv  48077  gpgcubic  48089  gpg5nbgr3star  48091  pgnbgreunbgrlem2  48127  pgnbgreunbgrlem5  48133  ellcoellss  48446  nn0sumshdiglem1  48632  itschlc0xyqsol  48778  itsclc0  48782  opnneilv  48919