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  1118  ralrimdva  3138  disjiun  5088  reusv3  5352  euotd  5469  swopo  5551  sotr3  5581  wereu2  5629  poirr2  6089  sossfld  6152  reuop  6259  frpomin  6306  oneqmini  6378  suctr  6413  elpreima  7012  fmptco  7084  isofrlem  7296  onmindif2  7762  resf1extb  7886  mptcnfimad  7940  frxp  8078  fnse  8085  suppss  8146  tposfo2  8201  wfr3g  8271  tz7.48-2  8383  omeulem1  8519  omeu  8522  nnaordex  8576  eldifsucnn  8602  pssnn  9105  onomeneq  9150  fodomfib  9241  fodomfibOLD  9243  dffi3  9346  supmo  9367  supnub  9377  infglb  9406  infnlb  9408  infmo  9412  infsupprpr  9421  cantnfle  9592  cantnflem1  9610  epfrs  9652  frr3g  9680  updjud  9858  alephord2i  9999  cardinfima  10019  aceq3lem  10042  dfac2b  10053  dfac12lem2  10067  axdc2lem  10370  ttukeylem6  10436  alephval2  10495  fpwwe2lem11  10564  fpwwe2lem12  10565  prlem934  10956  reclem4pr  10973  suplem1pr  10975  letr  11239  sup2  12110  uzind  12596  ledivge1le  12990  xrletr  13084  xltnegi  13143  xlemul1a  13215  ixxssixx  13287  difreicc  13412  flval3  13747  fsequb  13910  seqf1olem1  13976  expnegz  14031  hash2prd  14410  ccatrcl1  14530  relexprelg  14973  shftlem  15003  rexuzre  15288  cau3lem  15290  caubnd2  15293  caubnd  15294  climrlim2  15482  climuni  15487  2clim  15507  o1co  15521  rlimno1  15589  climbdd  15607  caurcvg  15612  summolem2  15651  summo  15652  zsum  15653  fsumf1o  15658  fsumss  15660  fsumcl2lem  15666  fsumadd  15675  fsummulc2  15719  fsumconst  15725  fsumrelem  15742  prodmolem2  15870  prodmo  15871  zprod  15872  fprodf1o  15881  fprodss  15883  fprodcl2lem  15885  fprodmul  15895  fproddiv  15896  fprodconst  15913  fprodn0  15914  dfgcd2  16485  lcmfunsnlem2  16579  coprmproddvdslem  16601  cncongrprm  16668  prmpwdvds  16844  infpnlem1  16850  1arith  16867  vdwapun  16914  vdwlem11  16931  vdwnnlem2  16936  ramz  16965  ramcl  16969  prmlem0  17045  firest  17364  catpropd  17644  initoid  17937  termoid  17938  initoeu2lem1  17950  pltnle  18271  pltletr  18276  pospo  18278  psss  18515  isgrpid2  18918  f1omvdco2  19389  pgpfi  19546  frgpnabllem1  19814  gsumval3eu  19845  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumzaddlem  19862  gsumconst  19875  gsumzmhm  19878  gsumzoppg  19885  ablfaclem3  20030  dvdsrtr  20316  dvdsrmul1  20317  unitgrp  20331  domnmuln0  20654  lspsolvlem  21109  gsumfsum  21401  nzerooringczr  21447  obslbs  21697  gsummoncoe1  22264  pf1ind  22311  dmatscmcl  22459  scmatmulcl  22474  smatvscl  22480  mdetdiaglem  22554  cpmatinvcl  22673  mp2pm2mplem4  22765  cpmadugsumlemF  22832  eltg3  22918  tgidm  22936  neindisj  23073  tgrest  23115  restcld  23128  tgcn  23208  lmcnp  23260  iunconnlem  23383  2ndcredom  23406  2ndc1stc  23407  1stcrest  23409  2ndcrest  23410  2ndcdisj  23412  nllyrest  23442  nllyidm  23445  lfinpfin  23480  locfincmp  23482  ptpjpre1  23527  ptuni2  23532  ptbasin  23533  ptbasfi  23537  txbasval  23562  ptpjopn  23568  ptclsg  23571  dfac14lem  23573  xkoccn  23575  txcnp  23576  ptcnplem  23577  ptcnp  23578  txtube  23596  txcmplem1  23597  txcmplem2  23598  tx2ndc  23607  txkgen  23608  xkoco1cn  23613  xkoco2cn  23614  xkococnlem  23615  xkococn  23616  xkoinjcn  23643  qtoprest  23673  kqsat  23687  kqcldsat  23689  isfild  23814  fbunfip  23825  fgabs  23835  filconn  23839  fbasrn  23840  filufint  23876  elfm2  23904  elfm3  23906  fmfnfm  23914  hausflimi  23936  cnpflfi  23955  ptcmplem2  24009  tmdgsum2  24052  cldsubg  24067  qustgpopn  24076  ustfilxp  24169  bldisj  24354  xbln0  24370  blssps  24380  blss  24381  blssexps  24382  blssex  24383  blcls  24462  metcnp3  24496  icccmplem2  24780  mpomulcn  24826  cnheibor  24922  iscau4  25247  cmssmscld  25318  ovolshftlem2  25479  ovolicc2lem5  25490  dyadmax  25567  mbfi1fseqlem4  25687  mbfi1flimlem  25691  lhop1lem  25986  dvfsumrlim  26006  aalioulem3  26310  ulmcn  26376  radcnvlt1  26395  pilem2  26430  efopn  26635  cxpeq0  26655  cxpmul2z  26668  cxpcn3lem  26725  xrlimcnp  26946  vmappw  27094  fsumvma  27192  dchrptlem1  27243  lgsqr  27330  lgsdchrval  27333  2lgslem3  27383  2sqlem6  27402  2sqlem7  27403  2sqreultlem  27426  2sqreunnltlem  27429  pntlem3  27588  pntleml  27590  ltsval2  27636  nosupno  27683  nosupbnd1lem5  27692  noinfno  27698  lestr  27742  madebdayim  27896  ltslpss  27916  negsid  28049  noseqinds  28301  brbtwn  28984  brcgr  28985  axcontlem8  29056  nbumgrvtx  29431  cusgrfilem2  29542  1loopgrnb0  29588  uspgr2wlkeq  29731  wlklenvclwlk  29739  upgrwlkdvdelem  29821  uspgrn2crct  29893  0enwwlksnge1  29949  usgr2wspthons3  30052  clwwlkccatlem  30076  clwlkclwwlkf  30095  clwwlknonel  30182  frgrncvvdeqlem9  30394  frgr2wwlkeqm  30418  frgrreggt1  30480  frgrreg  30481  pjhthmo  31389  spansncvi  31739  nmcexi  32113  cnlnssadj  32167  leopmuli  32220  elpjrn  32277  mdsl0  32397  sumdmdii  32502  fmptcof2  32746  suppss3  32812  lmxrge0  34129  bnj594  35087  bnj849  35100  noinfepfnregs  35307  subgrwlk  35345  erdszelem7  35410  sconnpi1  35452  cvmsval  35479  cvmopnlem  35491  cvmfolem  35492  cvmliftmolem2  35495  cvmlift2lem10  35525  cvmlift2lem12  35527  cvmlift3lem5  35536  cvmlift3lem8  35539  satfv0  35571  satfv1  35576  satfvsucsuc  35578  satffunlem1lem2  35616  satffunlem2lem2  35619  linethru  36366  opnrebl2  36534  neibastop2lem  36573  neibastop2  36574  bj-cbv3ta  37025  isinf2  37649  phpreu  37844  finixpnum  37845  lindsadd  37853  matunitlindflem1  37856  ptrecube  37860  poimirlem26  37886  poimirlem27  37887  poimirlem31  37891  poimir  37893  heicant  37895  voliunnfl  37904  volsupnfl  37905  itg2addnclem  37911  unirep  37954  sdclem2  37982  istotbnd3  38011  ssbnd  38028  eldisjlem19  39153  lshpdisj  39352  lsatn0  39364  lsat0cv  39398  cvrletrN  39638  cvrval4N  39779  lncvrelatN  40146  paddasslem14  40198  paddasslem15  40199  paddasslem16  40200  pmapjoin  40217  dihglblem2N  41659  dochvalr  41722  eqresfnbd  42593  sn-sup2  42850  prjspner1  42973  flt4lem7  43006  incssnn0  43057  eldioph4b  43157  diophren  43159  fphpdo  43163  rencldnfilem  43166  pellexlem5  43179  pell1234qrne0  43199  pell1234qrmulcl  43201  pell14qrgt0  43205  pell1234qrdich  43207  pell14qrdich  43215  pell1qrge1  43216  pell1qrgap  43220  pellfundre  43227  pellfundlb  43230  dvdsacongtr  43330  jm2.19lem4  43338  aomclem4  43403  hbtlem2  43470  hbtlem4  43472  hbtlem6  43475  cantnfresb  43670  dflim5  43675  tfsconcatrn  43688  tfsconcatrev  43694  naddwordnexlem4  43747  safesnsupfiss  43760  harval3  43883  clcnvlem  43968  ordpss  44795  relpfrlem  45298  cfsetsnfsetfo  47409  euoreqb  47458  2reu8i  47462  sprsymrelf1lem  47840  sprsymrelfolem2  47842  reupr  47871  fmtnofac2lem  47917  opoeALTV  48032  opeoALTV  48033  fpprwpprb  48089  gboge9  48113  clnbgrel  48177  grimco  48238  uhgrimedgi  48239  isuspgrim  48245  cycldlenngric  48277  uhgrimisgrgric  48280  clnbgrgrimlem  48282  clnbgrgrim  48283  grtriprop  48290  stgrusgra  48308  grlimedgclnbgr  48344  grlimprclnbgrvtx  48348  grlimgredgex  48349  grlictr  48364  gpgedg2iv  48416  gpgcubic  48428  gpg5nbgr3star  48430  pgnbgreunbgrlem2  48466  pgnbgreunbgrlem5  48472  ellcoellss  48784  nn0sumshdiglem1  48970  itschlc0xyqsol  49116  itsclc0  49120  opnneilv  49257