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  5074  reusv3  5348  euotd  5468  swopo  5550  sotr3  5580  wereu2  5628  poirr2  6088  sossfld  6151  reuop  6258  frpomin  6305  oneqmini  6377  suctr  6412  elpreima  7011  fmptco  7083  isofrlem  7295  onmindif2  7761  resf1extb  7885  mptcnfimad  7939  frxp  8076  fnse  8083  suppss  8144  tposfo2  8199  wfr3g  8269  tz7.48-2  8381  omeulem1  8517  omeu  8520  nnaordex  8574  eldifsucnn  8600  pssnn  9103  onomeneq  9148  fodomfib  9239  fodomfibOLD  9241  dffi3  9344  supmo  9365  supnub  9375  infglb  9404  infnlb  9406  infmo  9410  infsupprpr  9419  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  11240  sup2  12112  uzind  12621  ledivge1le  13015  xrletr  13109  xltnegi  13168  xlemul1a  13240  ixxssixx  13312  difreicc  13437  flval3  13774  fsequb  13937  seqf1olem1  14003  expnegz  14058  hash2prd  14437  ccatrcl1  14557  relexprelg  15000  shftlem  15030  rexuzre  15315  cau3lem  15317  caubnd2  15320  caubnd  15321  climrlim2  15509  climuni  15514  2clim  15534  o1co  15548  rlimno1  15616  climbdd  15634  caurcvg  15639  summolem2  15678  summo  15679  zsum  15680  fsumf1o  15685  fsumss  15687  fsumcl2lem  15693  fsumadd  15702  fsummulc2  15746  fsumconst  15752  fsumrelem  15770  prodmolem2  15900  prodmo  15901  zprod  15902  fprodf1o  15911  fprodss  15913  fprodcl2lem  15915  fprodmul  15925  fproddiv  15926  fprodconst  15943  fprodn0  15944  dfgcd2  16515  lcmfunsnlem2  16609  coprmproddvdslem  16631  cncongrprm  16699  prmpwdvds  16875  infpnlem1  16881  1arith  16898  vdwapun  16945  vdwlem11  16962  vdwnnlem2  16967  ramz  16996  ramcl  17000  prmlem0  17076  firest  17395  catpropd  17675  initoid  17968  termoid  17969  initoeu2lem1  17981  pltnle  18302  pltletr  18307  pospo  18309  psss  18546  isgrpid2  18952  f1omvdco2  19423  pgpfi  19580  frgpnabllem1  19848  gsumval3eu  19879  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumconst  19909  gsumzmhm  19912  gsumzoppg  19919  ablfaclem3  20064  dvdsrtr  20348  dvdsrmul1  20349  unitgrp  20363  domnmuln0  20686  lspsolvlem  21140  gsumfsum  21414  nzerooringczr  21460  obslbs  21710  gsummoncoe1  22273  pf1ind  22320  dmatscmcl  22468  scmatmulcl  22483  smatvscl  22489  mdetdiaglem  22563  cpmatinvcl  22682  mp2pm2mplem4  22774  cpmadugsumlemF  22841  eltg3  22927  tgidm  22945  neindisj  23082  tgrest  23124  restcld  23137  tgcn  23217  lmcnp  23269  iunconnlem  23392  2ndcredom  23415  2ndc1stc  23416  1stcrest  23418  2ndcrest  23419  2ndcdisj  23421  nllyrest  23451  nllyidm  23454  lfinpfin  23489  locfincmp  23491  ptpjpre1  23536  ptuni2  23541  ptbasin  23542  ptbasfi  23546  txbasval  23571  ptpjopn  23577  ptclsg  23580  dfac14lem  23582  xkoccn  23584  txcnp  23585  ptcnplem  23586  ptcnp  23587  txtube  23605  txcmplem1  23606  txcmplem2  23607  tx2ndc  23616  txkgen  23617  xkoco1cn  23622  xkoco2cn  23623  xkococnlem  23624  xkococn  23625  xkoinjcn  23652  qtoprest  23682  kqsat  23696  kqcldsat  23698  isfild  23823  fbunfip  23834  fgabs  23844  filconn  23848  fbasrn  23849  filufint  23885  elfm2  23913  elfm3  23915  fmfnfm  23923  hausflimi  23945  cnpflfi  23964  ptcmplem2  24018  tmdgsum2  24061  cldsubg  24076  qustgpopn  24085  ustfilxp  24178  bldisj  24363  xbln0  24379  blssps  24389  blss  24390  blssexps  24391  blssex  24392  blcls  24471  metcnp3  24505  icccmplem2  24789  mpomulcn  24834  cnheibor  24922  iscau4  25246  cmssmscld  25317  ovolshftlem2  25477  ovolicc2lem5  25488  dyadmax  25565  mbfi1fseqlem4  25685  mbfi1flimlem  25689  lhop1lem  25980  dvfsumrlim  25998  aalioulem3  26300  ulmcn  26364  radcnvlt1  26383  pilem2  26417  efopn  26622  cxpeq0  26642  cxpmul2z  26655  cxpcn3lem  26711  xrlimcnp  26932  vmappw  27079  fsumvma  27176  dchrptlem1  27227  lgsqr  27314  lgsdchrval  27317  2lgslem3  27367  2sqlem6  27386  2sqlem7  27387  2sqreultlem  27410  2sqreunnltlem  27413  pntlem3  27572  pntleml  27574  ltsval2  27620  nosupno  27667  nosupbnd1lem5  27676  noinfno  27682  lestr  27726  madebdayim  27880  ltslpss  27900  negsid  28033  noseqinds  28285  brbtwn  28968  brcgr  28969  axcontlem8  29040  nbumgrvtx  29415  cusgrfilem2  29525  1loopgrnb0  29571  uspgr2wlkeq  29714  wlklenvclwlk  29722  upgrwlkdvdelem  29804  uspgrn2crct  29876  0enwwlksnge1  29932  usgr2wspthons3  30035  clwwlkccatlem  30059  clwlkclwwlkf  30078  clwwlknonel  30165  frgrncvvdeqlem9  30377  frgr2wwlkeqm  30401  frgrreggt1  30463  frgrreg  30464  pjhthmo  31373  spansncvi  31723  nmcexi  32097  cnlnssadj  32151  leopmuli  32204  elpjrn  32261  mdsl0  32381  sumdmdii  32486  fmptcof2  32730  suppss3  32796  lmxrge0  34096  bnj594  35054  bnj849  35067  noinfepfnregs  35276  subgrwlk  35314  erdszelem7  35379  sconnpi1  35421  cvmsval  35448  cvmopnlem  35460  cvmfolem  35461  cvmliftmolem2  35464  cvmlift2lem10  35494  cvmlift2lem12  35496  cvmlift3lem5  35505  cvmlift3lem8  35508  satfv0  35540  satfv1  35545  satfvsucsuc  35547  satffunlem1lem2  35585  satffunlem2lem2  35588  linethru  36335  opnrebl2  36503  neibastop2lem  36542  neibastop2  36543  bj-cbv3ta  37093  cgsex2gd  37451  isinf2  37721  phpreu  37925  finixpnum  37926  lindsadd  37934  matunitlindflem1  37937  ptrecube  37941  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  poimir  37974  heicant  37976  voliunnfl  37985  volsupnfl  37986  itg2addnclem  37992  unirep  38035  sdclem2  38063  istotbnd3  38092  ssbnd  38109  eldisjlem19  39234  lshpdisj  39433  lsatn0  39445  lsat0cv  39479  cvrletrN  39719  cvrval4N  39860  lncvrelatN  40227  paddasslem14  40279  paddasslem15  40280  paddasslem16  40281  pmapjoin  40298  dihglblem2N  41740  dochvalr  41803  eqresfnbd  42673  sn-sup2  42936  prjspner1  43059  flt4lem7  43092  incssnn0  43143  eldioph4b  43239  diophren  43241  fphpdo  43245  rencldnfilem  43248  pellexlem5  43261  pell1234qrne0  43281  pell1234qrmulcl  43283  pell14qrgt0  43287  pell1234qrdich  43289  pell14qrdich  43297  pell1qrge1  43298  pell1qrgap  43302  pellfundre  43309  pellfundlb  43312  dvdsacongtr  43412  jm2.19lem4  43420  aomclem4  43485  hbtlem2  43552  hbtlem4  43554  hbtlem6  43557  cantnfresb  43752  dflim5  43757  tfsconcatrn  43770  tfsconcatrev  43776  naddwordnexlem4  43829  safesnsupfiss  43842  harval3  43965  clcnvlem  44050  ordpss  44877  relpfrlem  45380  cfsetsnfsetfo  47502  euoreqb  47551  2reu8i  47555  sprsymrelf1lem  47945  sprsymrelfolem2  47947  reupr  47976  fmtnofac2lem  48025  opoeALTV  48153  opeoALTV  48154  fpprwpprb  48210  gboge9  48234  clnbgrel  48298  grimco  48359  uhgrimedgi  48360  isuspgrim  48366  cycldlenngric  48398  uhgrimisgrgric  48401  clnbgrgrimlem  48403  clnbgrgrim  48404  grtriprop  48411  stgrusgra  48429  grlimedgclnbgr  48465  grlimprclnbgrvtx  48469  grlimgredgex  48470  grlictr  48485  gpgedg2iv  48537  gpgcubic  48549  gpg5nbgr3star  48551  pgnbgreunbgrlem2  48587  pgnbgreunbgrlem5  48593  ellcoellss  48905  nn0sumshdiglem1  49091  itschlc0xyqsol  49237  itsclc0  49241  opnneilv  49378