Theorem expimpd 456

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ornld  1056  3impia  1113  ralrimdva  3189  disjiun  5052  reusv3  5305  euotd  5402  swopo  5483  wereu2  5551  poirr2  5983  sossfld  6042  reuop  6143  oneqmini  6241  suctr  6273  elpreima  6827  fmptco  6890  isofrlem  7092  onmindif2  7526  frxp  7819  fnse  7826  suppss  7859  tposfo2  7914  wfr3g  7952  tz7.48-2  8077  omeulem1  8207  omeu  8210  nnaordex  8263  pssnn  8735  fodomfib  8797  dffi3  8894  supmo  8915  supnub  8925  infglb  8953  infnlb  8955  infmo  8958  infsupprpr  8967  cantnfle  9133  cantnflem1  9151  epfrs  9172  updjud  9362  alephord2i  9502  cardinfima  9522  aceq3lem  9545  dfac2b  9555  dfac12lem2  9569  axdc2lem  9869  ttukeylem6  9935  alephval2  9993  fpwwe2lem12  10062  fpwwe2lem13  10063  prlem934  10454  reclem4pr  10471  suplem1pr  10473  letr  10733  sup2  11596  uzind  12073  ledivge1le  12459  xrletr  12550  xltnegi  12608  xlemul1a  12680  ixxssixx  12751  difreicc  12869  flval3  13184  fsequb  13342  seqf1olem1  13408  expnegz  13462  hash2prd  13832  ccatrcl1  13947  relexprelg  14396  shftlem  14426  rexuzre  14711  cau3lem  14713  caubnd2  14716  caubnd  14717  climrlim2  14903  climuni  14908  2clim  14928  o1co  14942  rlimno1  15009  climbdd  15027  caurcvg  15032  summolem2  15072  summo  15073  zsum  15074  fsumf1o  15079  fsumss  15081  fsumcl2lem  15087  fsumadd  15095  fsummulc2  15138  fsumconst  15144  fsumrelem  15161  prodmolem2  15288  prodmo  15289  zprod  15290  fprodf1o  15299  fprodss  15301  fprodcl2lem  15303  fprodmul  15313  fproddiv  15314  fprodconst  15331  fprodn0  15332  dfgcd2  15893  lcmfunsnlem2  15983  coprmproddvdslem  16005  cncongrprm  16068  prmpwdvds  16239  infpnlem1  16245  1arith  16262  vdwapun  16309  vdwlem11  16326  vdwnnlem2  16331  ramz  16360  ramcl  16364  prmlem0  16438  firest  16705  catpropd  16978  initoid  17264  termoid  17265  initoeu2lem1  17273  pltnle  17575  pltletr  17580  pospo  17582  psss  17823  isgrpid2  18139  f1omvdco2  18575  pgpfi  18729  frgpnabllem1  18992  gsumval3eu  19023  gsumzres  19028  gsumzcl2  19029  gsumzf1o  19031  gsumzaddlem  19040  gsumconst  19053  gsumzmhm  19056  gsumzoppg  19063  ablfaclem3  19208  dvdsrtr  19401  dvdsrmul1  19402  unitgrp  19416  lspsolvlem  19913  domnmuln0  20070  gsummoncoe1  20471  pf1ind  20517  gsumfsum  20611  obslbs  20873  dmatscmcl  21111  scmatmulcl  21126  smatvscl  21132  mdetdiaglem  21206  cpmatinvcl  21324  mp2pm2mplem4  21416  cpmadugsumlemF  21483  eltg3  21569  tgidm  21587  neindisj  21724  tgrest  21766  restcld  21779  tgcn  21859  lmcnp  21911  iunconnlem  22034  2ndcredom  22057  2ndc1stc  22058  1stcrest  22060  2ndcrest  22061  2ndcdisj  22063  nllyrest  22093  nllyidm  22096  lfinpfin  22131  locfincmp  22133  ptpjpre1  22178  ptuni2  22183  ptbasin  22184  ptbasfi  22188  txbasval  22213  ptpjopn  22219  ptclsg  22222  dfac14lem  22224  xkoccn  22226  txcnp  22227  ptcnplem  22228  ptcnp  22229  txtube  22247  txcmplem1  22248  txcmplem2  22249  tx2ndc  22258  txkgen  22259  xkoco1cn  22264  xkoco2cn  22265  xkococnlem  22266  xkococn  22267  xkoinjcn  22294  qtoprest  22324  kqsat  22338  kqcldsat  22340  isfild  22465  fbunfip  22476  fgabs  22486  filconn  22490  fbasrn  22491  filufint  22527  elfm2  22555  elfm3  22557  fmfnfm  22565  hausflimi  22587  cnpflfi  22606  ptcmplem2  22660  tmdgsum2  22703  cldsubg  22718  qustgpopn  22727  ustfilxp  22820  bldisj  23007  xbln0  23023  blssps  23033  blss  23034  blssexps  23035  blssex  23036  blcls  23115  metcnp3  23149  icccmplem2  23430  cnheibor  23558  iscau4  23881  cmssmscld  23952  ovolshftlem2  24110  ovolicc2lem5  24121  dyadmax  24198  mbfi1fseqlem4  24318  mbfi1flimlem  24322  lhop1lem  24609  dvfsumrlim  24627  aalioulem3  24922  ulmcn  24986  radcnvlt1  25005  pilem2  25039  efopn  25240  cxpeq0  25260  cxpmul2z  25273  cxpcn3lem  25327  xrlimcnp  25545  vmappw  25692  fsumvma  25788  dchrptlem1  25839  lgsqr  25926  lgsdchrval  25929  2lgslem3  25979  2sqlem6  25998  2sqlem7  25999  2sqreultlem  26022  2sqreunnltlem  26025  pntlem3  26184  pntleml  26186  brbtwn  26684  brcgr  26685  axcontlem8  26756  nbumgrvtx  27127  cusgrfilem2  27237  1loopgrnb0  27283  uspgr2wlkeq  27426  wlklenvclwlk  27435  upgrwlkdvdelem  27516  uspgrn2crct  27585  0enwwlksnge1  27641  usgr2wspthons3  27742  clwwlkccatlem  27766  clwlkclwwlkf  27785  clwwlknonel  27873  frgrncvvdeqlem9  28085  frgr2wwlkeqm  28109  frgrreggt1  28171  frgrreg  28172  pjhthmo  29078  spansncvi  29428  nmcexi  29802  cnlnssadj  29856  leopmuli  29909  elpjrn  29966  mdsl0  30086  sumdmdii  30191  fmptcof2  30401  suppss3  30459  lmxrge0  31195  bnj594  32184  bnj849  32197  subgrwlk  32379  erdszelem7  32444  sconnpi1  32486  cvmsval  32513  cvmopnlem  32525  cvmfolem  32526  cvmliftmolem2  32529  cvmlift2lem10  32559  cvmlift2lem12  32561  cvmlift3lem5  32570  cvmlift3lem8  32573  satfv0  32605  satfv1  32610  satfvsucsuc  32612  satffunlem1lem2  32650  satffunlem2lem2  32653  sotr3  33002  trpredrec  33077  frpomin  33078  frr3g  33121  sltval2  33163  nosupno  33203  nosupbnd1lem5  33212  sletr  33237  linethru  33614  opnrebl2  33669  neibastop2lem  33708  neibastop2  33709  bj-cbv3ta  34108  isinf2  34685  phpreu  34875  finixpnum  34876  lindsadd  34884  matunitlindflem1  34887  ptrecube  34891  poimirlem26  34917  poimirlem27  34918  poimirlem31  34922  poimir  34924  heicant  34926  voliunnfl  34935  volsupnfl  34936  itg2addnclem  34942  unirep  34987  sdclem2  35016  istotbnd3  35048  ssbnd  35065  lshpdisj  36122  lsatn0  36134  lsat0cv  36168  cvrletrN  36408  cvrval4N  36549  lncvrelatN  36916  paddasslem14  36968  paddasslem15  36969  paddasslem16  36970  pmapjoin  36987  dihglblem2N  38429  dochvalr  38492  incssnn0  39306  eldioph4b  39406  diophren  39408  fphpdo  39412  rencldnfilem  39415  pellexlem5  39428  pell1234qrne0  39448  pell1234qrmulcl  39450  pell14qrgt0  39454  pell1234qrdich  39456  pell14qrdich  39464  pell1qrge1  39465  pell1qrgap  39469  pellfundre  39476  pellfundlb  39479  dvdsacongtr  39579  jm2.19lem4  39587  aomclem4  39655  hbtlem2  39722  hbtlem4  39724  hbtlem6  39727  harval3  39902  clcnvlem  39981  ordpss  40781  euoreqb  43307  2reu8i  43311  sprsymrelf1lem  43652  sprsymrelfolem2  43654  reupr  43683  fmtnofac2lem  43729  opoeALTV  43847  opeoALTV  43848  fpprwpprb  43904  gboge9  43928  nzerooringczr  44342  ellcoellss  44489  nn0sumshdiglem1  44680  itschlc0xyqsol  44753  itsclc0  44757