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 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  ornld  1076  3impia  1134  ralrimdva  3164  disjiun  5096  reusv3  5375  euotd  5495  swopo  5579  sotr3  5609  wereu2  5657  poirr2  6123  sossfld  6183  reuop  6294  frpomin  6341  ordpss  6389  oneqmini  6414  suctr  6449  elpreima  7053  fmptco  7125  isofrlem  7338  onmindif2  7804  resf1extb  7929  mptcnfimad  7981  frxp  8120  fnse  8127  suppss  8188  tposfo2  8243  wfr3g  8314  tz7.48-2  8427  omeulem1  8565  omeu  8568  nnaordex  8622  eldifsucnn  8648  pssnn  9151  onomeneq  9196  fodomfib  9286  dffi3  9389  supmo  9410  supnub  9420  infglb  9449  infnlb  9451  infmo  9455  infsupprpr  9464  cantnfle  9638  cantnflem1  9656  epfrs  9698  frr3g  9726  updjud  9927  alephord2i  10068  cardinfima  10088  aceq3lem  10111  dfac2b  10121  dfac12lem2  10135  axdc2lem  10438  ttukeylem6  10504  alephval2  10563  fpwwe2lem11  10632  fpwwe2lem12  10633  prlem934  11024  reclem4pr  11041  suplem1pr  11043  letr  11310  sup2  12177  uzind  12694  ledivge1le  13095  xrletr  13189  xltnegi  13248  xlemul1a  13320  ixxssixx  13392  difreicc  13517  flval3  13855  fsequb  14018  seqf1olem1  14084  expnegz  14139  hash2prd  14519  ccatrcl1  14639  relexprelg  15082  shftlem  15112  rexuzre  15411  cau3lem  15413  caubnd2  15416  caubnd  15417  climrlim2  15605  climuni  15610  2clim  15630  o1co  15644  rlimno1  15712  climbdd  15730  caurcvg  15735  summolem2  15774  summo  15775  zsum  15776  fsumf1o  15781  fsumss  15783  fsumcl2lem  15789  fsumadd  15798  fsummulc2  15842  fsumconst  15848  fsumrelem  15866  prodmolem2  15996  prodmo  15997  zprod  15998  fprodf1o  16007  fprodss  16009  fprodcl2lem  16011  fprodmul  16021  fproddiv  16022  fprodconst  16039  fprodn0  16040  dfgcd2  16610  lcmfunsnlem2  16704  coprmproddvdslem  16726  cncongrprm  16794  prmpwdvds  16970  infpnlem1  16976  1arith  16993  vdwapun  17040  vdwlem11  17057  vdwnnlem2  17062  ramz  17091  ramcl  17095  prmlem0  17171  firest  17491  catpropd  17771  initoid  18064  termoid  18065  initoeu2lem1  18077  pltnle  18398  pltletr  18403  pospo  18405  psss  18642  isgrpid2  19049  f1omvdco2  19524  pgpfi  19681  frgpnabllem1  19949  gsumval3eu  19980  gsumzres  19985  gsumzcl2  19986  gsumzf1o  19988  gsumzaddlem  19997  gsumconst  20010  gsumzmhm  20013  gsumzoppg  20020  ablfaclem3  20165  dvdsrtr  20457  dvdsrmul1  20458  unitgrp  20472  domnmuln0  20819  lspsolvlem  21277  gsumfsum  21595  nzerooringczr  21641  obslbs  21891  gsummoncoe1  22479  pf1ind  22526  dmatscmcl  22671  scmatmulcl  22686  smatvscl  22692  mdetdiaglem  22766  cpmatinvcl  22885  mp2pm2mplem4  22977  cpmadugsumlemF  23044  eltg3  23130  tgidm  23148  neindisj  23285  tgrest  23327  restcld  23340  tgcn  23420  lmcnp  23472  iunconnlem  23595  2ndcredom  23618  2ndc1stc  23619  1stcrest  23621  2ndcrest  23622  2ndcdisj  23624  nllyrest  23654  nllyidm  23657  lfinpfin  23692  locfincmp  23694  ptpjpre1  23739  ptuni2  23744  ptbasin  23745  ptbasfi  23749  txbasval  23774  ptpjopn  23780  ptclsg  23783  dfac14lem  23785  xkoccn  23787  txcnp  23788  ptcnplem  23789  ptcnp  23790  txtube  23808  txcmplem1  23809  txcmplem2  23810  tx2ndc  23819  txkgen  23820  xkoco1cn  23825  xkoco2cn  23826  xkococnlem  23827  xkococn  23828  xkoinjcn  23855  qtoprest  23885  kqsat  23899  kqcldsat  23901  isfild  24026  fbunfip  24037  fgabs  24047  filconn  24051  fbasrn  24052  filufint  24088  elfm2  24116  elfm3  24118  fmfnfm  24126  hausflimi  24148  cnpflfi  24167  ptcmplem2  24221  tmdgsum2  24264  cldsubg  24279  qustgpopn  24288  ustfilxp  24381  bldisj  24566  xbln0  24582  blssps  24592  blss  24593  blssexps  24594  blssex  24595  blcls  24674  metcnp3  24708  icccmplem2  24992  mpomulcn  25037  cnheibor  25125  iscau4  25449  cmssmscld  25520  ovolshftlem2  25680  ovolicc2lem5  25691  dyadmax  25768  mbfi1fseqlem4  25888  mbfi1flimlem  25892  lhop1lem  26183  dvfsumrlim  26201  aalioulem3  26508  ulmcn  26573  radcnvlt1  26592  pilem2  26626  efopn  26834  cxpeq0  26854  cxpmul2z  26867  cxpcn3lem  26923  xrlimcnp  27144  vmappw  27291  fsumvma  27388  dchrptlem1  27439  lgsqr  27526  lgsdchrval  27529  2lgslem3  27579  2sqlem6  27598  2sqlem7  27599  2sqreultlem  27622  2sqreunnltlem  27625  pntlem3  27784  pntleml  27786  ltsval2  27831  nosupno  27878  nosupbnd1lem5  27887  noinfno  27893  lestr  27937  madebdayim  28092  ltslpss  28112  negsid  28245  noseqinds  28497  brbtwn  29260  brcgr  29261  axcontlem8  29332  nbumgrvtx  29707  cusgrfilem2  29817  1loopgrnb0  29863  uspgr2wlkeq  30006  wlklenvclwlk  30014  upgrwlkdvdelem  30096  uspgrn2crct  30168  0enwwlksnge1  30224  usgr2wspthons3  30327  clwwlkccatlem  30351  clwlkclwwlkf  30370  clwwlknonel  30457  frgrncvvdeqlem9  30669  frgr2wwlkeqm  30693  frgrreggt1  30755  frgrreg  30756  pjhthmo  31665  spansncvi  32015  nmcexi  32389  cnlnssadj  32443  leopmuli  32496  elpjrn  32553  mdsl0  32673  sumdmdii  32778  fmptcof2  33013  suppss3  33079  lmxrge0  34351  bnj594  35309  bnj849  35322  noinfepfnregs  35553  subgrwlk  35632  erdszelem7  35697  sconnpi1  35739  cvmsval  35766  cvmopnlem  35778  cvmfolem  35779  cvmliftmolem2  35782  cvmlift2lem10  35812  cvmlift2lem12  35814  cvmlift3lem5  35823  cvmlift3lem8  35826  satfv0  35858  satfv1  35863  satfvsucsuc  35865  satffunlem1lem2  35903  satffunlem2lem2  35906  linethru  36653  opnrebl2  36860  neibastop2lem  36899  neibastop2  36900  bj-cbv3ta  37449  cgsex2gd  37809  isinf2  38079  phpreu  38283  finixpnum  38284  lindsadd  38292  matunitlindflem1  38295  ptrecube  38299  poimirlem26  38325  poimirlem27  38326  poimirlem31  38330  poimir  38332  heicant  38334  voliunnfl  38343  volsupnfl  38344  itg2addnclem  38350  unirep  38393  sdclem2  38421  istotbnd3  38450  ssbnd  38467  eldisjlem19  39590  lshpdisj  39789  lsatn0  39801  lsat0cv  39835  cvrletrN  40075  cvrval4N  40216  lncvrelatN  40583  paddasslem14  40635  paddasslem15  40636  paddasslem16  40637  pmapjoin  40654  dihglblem2N  42096  dochvalr  42159  eqresfnbd  43031  sn-sup2  43293  prjspner1  43386  flt4lem7  43419  incssnn0  43470  eldioph4b  43566  diophren  43568  fphpdo  43572  rencldnfilem  43575  pellexlem5  43588  pell1234qrne0  43608  pell1234qrmulcl  43610  pell14qrgt0  43614  pell1234qrdich  43616  pell14qrdich  43624  pell1qrge1  43625  pell1qrgap  43629  pellfundre  43636  pellfundlb  43639  dvdsacongtr  43739  jm2.19lem4  43747  aomclem4  43812  hbtlem2  43879  hbtlem4  43881  hbtlem6  43884  cantnfresb  44079  dflim5  44084  tfsconcatrn  44097  tfsconcatrev  44103  naddwordnexlem4  44156  safesnsupfiss  44169  harval3  44292  clcnvlem  44377  relpfrlem  45690  cfsetsnfsetfo  47825  euoreqb  47874  2reu8i  47878  sprsymrelf1lem  48268  sprsymrelfolem2  48270  reupr  48299  fmtnofac2lem  48348  opoeALTV  48476  opeoALTV  48477  fpprwpprb  48533  gboge9  48557  clnbgrel  48621  grimco  48682  uhgrimedgi  48683  isuspgrim  48689  cycldlenngric  48721  uhgrimisgrgric  48724  clnbgrgrimlem  48726  clnbgrgrim  48727  grtriprop  48734  stgrusgra  48752  grlimedgclnbgr  48788  grlimprclnbgrvtx  48792  grlimgredgex  48793  grlictr  48808  gpgedg2iv  48860  gpgcubic  48872  gpg5nbgr3star  48874  pgnbgreunbgrlem2  48910  pgnbgreunbgrlem5  48916  ellcoellss  49243  nn0sumshdiglem1  49429  itschlc0xyqsol  49575  itsclc0  49579  opnneilv  49715