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  3134  disjiun  5098  reusv3  5363  euotd  5476  swopo  5560  sotr3  5590  wereu2  5638  poirr2  6100  sossfld  6162  reuop  6269  frpomin  6316  oneqmini  6388  suctr  6423  elpreima  7033  fmptco  7104  isofrlem  7318  onmindif2  7786  resf1extb  7913  mptcnfimad  7968  frxp  8108  fnse  8115  suppss  8176  tposfo2  8231  wfr3g  8301  tz7.48-2  8413  omeulem1  8549  omeu  8552  nnaordex  8605  eldifsucnn  8631  pssnn  9138  onomeneq  9184  fodomfib  9287  fodomfibOLD  9289  dffi3  9389  supmo  9410  supnub  9420  infglb  9449  infnlb  9451  infmo  9455  infsupprpr  9464  cantnfle  9631  cantnflem1  9649  epfrs  9691  frr3g  9716  updjud  9894  alephord2i  10037  cardinfima  10057  aceq3lem  10080  dfac2b  10091  dfac12lem2  10105  axdc2lem  10408  ttukeylem6  10474  alephval2  10532  fpwwe2lem11  10601  fpwwe2lem12  10602  prlem934  10993  reclem4pr  11010  suplem1pr  11012  letr  11275  sup2  12146  uzind  12633  ledivge1le  13031  xrletr  13125  xltnegi  13183  xlemul1a  13255  ixxssixx  13327  difreicc  13452  flval3  13784  fsequb  13947  seqf1olem1  14013  expnegz  14068  hash2prd  14447  ccatrcl1  14566  relexprelg  15011  shftlem  15041  rexuzre  15326  cau3lem  15328  caubnd2  15331  caubnd  15332  climrlim2  15520  climuni  15525  2clim  15545  o1co  15559  rlimno1  15627  climbdd  15645  caurcvg  15650  summolem2  15689  summo  15690  zsum  15691  fsumf1o  15696  fsumss  15698  fsumcl2lem  15704  fsumadd  15713  fsummulc2  15757  fsumconst  15763  fsumrelem  15780  prodmolem2  15908  prodmo  15909  zprod  15910  fprodf1o  15919  fprodss  15921  fprodcl2lem  15923  fprodmul  15933  fproddiv  15934  fprodconst  15951  fprodn0  15952  dfgcd2  16523  lcmfunsnlem2  16617  coprmproddvdslem  16639  cncongrprm  16706  prmpwdvds  16882  infpnlem1  16888  1arith  16905  vdwapun  16952  vdwlem11  16969  vdwnnlem2  16974  ramz  17003  ramcl  17007  prmlem0  17083  firest  17402  catpropd  17677  initoid  17970  termoid  17971  initoeu2lem1  17983  pltnle  18304  pltletr  18309  pospo  18311  psss  18546  isgrpid2  18915  f1omvdco2  19385  pgpfi  19542  frgpnabllem1  19810  gsumval3eu  19841  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumzaddlem  19858  gsumconst  19871  gsumzmhm  19874  gsumzoppg  19881  ablfaclem3  20026  dvdsrtr  20284  dvdsrmul1  20285  unitgrp  20299  domnmuln0  20625  lspsolvlem  21059  gsumfsum  21358  nzerooringczr  21397  obslbs  21646  gsummoncoe1  22202  pf1ind  22249  dmatscmcl  22397  scmatmulcl  22412  smatvscl  22418  mdetdiaglem  22492  cpmatinvcl  22611  mp2pm2mplem4  22703  cpmadugsumlemF  22770  eltg3  22856  tgidm  22874  neindisj  23011  tgrest  23053  restcld  23066  tgcn  23146  lmcnp  23198  iunconnlem  23321  2ndcredom  23344  2ndc1stc  23345  1stcrest  23347  2ndcrest  23348  2ndcdisj  23350  nllyrest  23380  nllyidm  23383  lfinpfin  23418  locfincmp  23420  ptpjpre1  23465  ptuni2  23470  ptbasin  23471  ptbasfi  23475  txbasval  23500  ptpjopn  23506  ptclsg  23509  dfac14lem  23511  xkoccn  23513  txcnp  23514  ptcnplem  23515  ptcnp  23516  txtube  23534  txcmplem1  23535  txcmplem2  23536  tx2ndc  23545  txkgen  23546  xkoco1cn  23551  xkoco2cn  23552  xkococnlem  23553  xkococn  23554  xkoinjcn  23581  qtoprest  23611  kqsat  23625  kqcldsat  23627  isfild  23752  fbunfip  23763  fgabs  23773  filconn  23777  fbasrn  23778  filufint  23814  elfm2  23842  elfm3  23844  fmfnfm  23852  hausflimi  23874  cnpflfi  23893  ptcmplem2  23947  tmdgsum2  23990  cldsubg  24005  qustgpopn  24014  ustfilxp  24107  bldisj  24293  xbln0  24309  blssps  24319  blss  24320  blssexps  24321  blssex  24322  blcls  24401  metcnp3  24435  icccmplem2  24719  mpomulcn  24765  cnheibor  24861  iscau4  25186  cmssmscld  25257  ovolshftlem2  25418  ovolicc2lem5  25429  dyadmax  25506  mbfi1fseqlem4  25626  mbfi1flimlem  25630  lhop1lem  25925  dvfsumrlim  25945  aalioulem3  26249  ulmcn  26315  radcnvlt1  26334  pilem2  26369  efopn  26574  cxpeq0  26594  cxpmul2z  26607  cxpcn3lem  26664  xrlimcnp  26885  vmappw  27033  fsumvma  27131  dchrptlem1  27182  lgsqr  27269  lgsdchrval  27272  2lgslem3  27322  2sqlem6  27341  2sqlem7  27342  2sqreultlem  27365  2sqreunnltlem  27368  pntlem3  27527  pntleml  27529  sltval2  27575  nosupno  27622  nosupbnd1lem5  27631  noinfno  27637  sletr  27677  madebdayim  27806  sltlpss  27826  negsid  27954  noseqinds  28194  brbtwn  28833  brcgr  28834  axcontlem8  28905  nbumgrvtx  29280  cusgrfilem2  29391  1loopgrnb0  29437  uspgr2wlkeq  29581  wlklenvclwlk  29590  upgrwlkdvdelem  29673  uspgrn2crct  29745  0enwwlksnge1  29801  usgr2wspthons3  29901  clwwlkccatlem  29925  clwlkclwwlkf  29944  clwwlknonel  30031  frgrncvvdeqlem9  30243  frgr2wwlkeqm  30267  frgrreggt1  30329  frgrreg  30330  pjhthmo  31238  spansncvi  31588  nmcexi  31962  cnlnssadj  32016  leopmuli  32069  elpjrn  32126  mdsl0  32246  sumdmdii  32351  fmptcof2  32588  suppss3  32654  lmxrge0  33949  bnj594  34909  bnj849  34922  subgrwlk  35126  erdszelem7  35191  sconnpi1  35233  cvmsval  35260  cvmopnlem  35272  cvmfolem  35273  cvmliftmolem2  35276  cvmlift2lem10  35306  cvmlift2lem12  35308  cvmlift3lem5  35317  cvmlift3lem8  35320  satfv0  35352  satfv1  35357  satfvsucsuc  35359  satffunlem1lem2  35397  satffunlem2lem2  35400  linethru  36148  opnrebl2  36316  neibastop2lem  36355  neibastop2  36356  bj-cbv3ta  36781  isinf2  37400  phpreu  37605  finixpnum  37606  lindsadd  37614  matunitlindflem1  37617  ptrecube  37621  poimirlem26  37647  poimirlem27  37648  poimirlem31  37652  poimir  37654  heicant  37656  voliunnfl  37665  volsupnfl  37666  itg2addnclem  37672  unirep  37715  sdclem2  37743  istotbnd3  37772  ssbnd  37789  eldisjlem19  38809  lshpdisj  38987  lsatn0  38999  lsat0cv  39033  cvrletrN  39273  cvrval4N  39415  lncvrelatN  39782  paddasslem14  39834  paddasslem15  39835  paddasslem16  39836  pmapjoin  39853  dihglblem2N  41295  dochvalr  41358  eqresfnbd  42227  sn-sup2  42486  prjspner1  42621  flt4lem7  42654  incssnn0  42706  eldioph4b  42806  diophren  42808  fphpdo  42812  rencldnfilem  42815  pellexlem5  42828  pell1234qrne0  42848  pell1234qrmulcl  42850  pell14qrgt0  42854  pell1234qrdich  42856  pell14qrdich  42864  pell1qrge1  42865  pell1qrgap  42869  pellfundre  42876  pellfundlb  42879  dvdsacongtr  42980  jm2.19lem4  42988  aomclem4  43053  hbtlem2  43120  hbtlem4  43122  hbtlem6  43125  cantnfresb  43320  dflim5  43325  tfsconcatrn  43338  tfsconcatrev  43344  naddwordnexlem4  43397  safesnsupfiss  43411  harval3  43534  clcnvlem  43619  ordpss  44447  relpfrlem  44950  cfsetsnfsetfo  47065  euoreqb  47114  2reu8i  47118  sprsymrelf1lem  47496  sprsymrelfolem2  47498  reupr  47527  fmtnofac2lem  47573  opoeALTV  47688  opeoALTV  47689  fpprwpprb  47745  gboge9  47769  clnbgrel  47833  grimco  47893  uhgrimedgi  47894  isuspgrim  47900  cycldlenngric  47932  uhgrimisgrgric  47935  clnbgrgrimlem  47937  clnbgrgrim  47938  grtriprop  47944  stgrusgra  47962  grlictr  48011  gpgedg2iv  48062  gpgcubic  48074  gpg5nbgr3star  48076  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem5  48117  ellcoellss  48428  nn0sumshdiglem1  48614  itschlc0xyqsol  48760  itsclc0  48764  opnneilv  48901