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  3141  disjiun  5112  reusv3  5380  euotd  5493  swopo  5577  sotr3  5607  wereu2  5656  poirr2  6118  sossfld  6180  reuop  6287  frpomin  6334  oneqmini  6410  suctr  6445  elpreima  7053  fmptco  7124  isofrlem  7338  onmindif2  7806  resf1extb  7935  mptcnfimad  7990  frxp  8130  fnse  8137  suppss  8198  tposfo2  8253  wfr3g  8326  tz7.48-2  8461  omeulem1  8599  omeu  8602  nnaordex  8655  eldifsucnn  8681  pssnn  9187  onomeneq  9242  fodomfib  9346  fodomfibOLD  9348  dffi3  9448  supmo  9469  supnub  9479  infglb  9508  infnlb  9510  infmo  9514  infsupprpr  9523  cantnfle  9690  cantnflem1  9708  epfrs  9750  frr3g  9775  updjud  9953  alephord2i  10096  cardinfima  10116  aceq3lem  10139  dfac2b  10150  dfac12lem2  10164  axdc2lem  10467  ttukeylem6  10533  alephval2  10591  fpwwe2lem11  10660  fpwwe2lem12  10661  prlem934  11052  reclem4pr  11069  suplem1pr  11071  letr  11334  sup2  12203  uzind  12690  ledivge1le  13085  xrletr  13179  xltnegi  13237  xlemul1a  13309  ixxssixx  13381  difreicc  13506  flval3  13837  fsequb  13998  seqf1olem1  14064  expnegz  14119  hash2prd  14498  ccatrcl1  14617  relexprelg  15062  shftlem  15092  rexuzre  15376  cau3lem  15378  caubnd2  15381  caubnd  15382  climrlim2  15568  climuni  15573  2clim  15593  o1co  15607  rlimno1  15675  climbdd  15693  caurcvg  15698  summolem2  15737  summo  15738  zsum  15739  fsumf1o  15744  fsumss  15746  fsumcl2lem  15752  fsumadd  15761  fsummulc2  15805  fsumconst  15811  fsumrelem  15828  prodmolem2  15956  prodmo  15957  zprod  15958  fprodf1o  15967  fprodss  15969  fprodcl2lem  15971  fprodmul  15981  fproddiv  15982  fprodconst  15999  fprodn0  16000  dfgcd2  16570  lcmfunsnlem2  16664  coprmproddvdslem  16686  cncongrprm  16753  prmpwdvds  16929  infpnlem1  16935  1arith  16952  vdwapun  16999  vdwlem11  17016  vdwnnlem2  17021  ramz  17050  ramcl  17054  prmlem0  17130  firest  17451  catpropd  17726  initoid  18019  termoid  18020  initoeu2lem1  18032  pltnle  18353  pltletr  18358  pospo  18360  psss  18595  isgrpid2  18964  f1omvdco2  19434  pgpfi  19591  frgpnabllem1  19859  gsumval3eu  19890  gsumzres  19895  gsumzcl2  19896  gsumzf1o  19898  gsumzaddlem  19907  gsumconst  19920  gsumzmhm  19923  gsumzoppg  19930  ablfaclem3  20075  dvdsrtr  20333  dvdsrmul1  20334  unitgrp  20348  domnmuln0  20674  lspsolvlem  21108  gsumfsum  21407  nzerooringczr  21446  obslbs  21695  gsummoncoe1  22251  pf1ind  22298  dmatscmcl  22446  scmatmulcl  22461  smatvscl  22467  mdetdiaglem  22541  cpmatinvcl  22660  mp2pm2mplem4  22752  cpmadugsumlemF  22819  eltg3  22905  tgidm  22923  neindisj  23060  tgrest  23102  restcld  23115  tgcn  23195  lmcnp  23247  iunconnlem  23370  2ndcredom  23393  2ndc1stc  23394  1stcrest  23396  2ndcrest  23397  2ndcdisj  23399  nllyrest  23429  nllyidm  23432  lfinpfin  23467  locfincmp  23469  ptpjpre1  23514  ptuni2  23519  ptbasin  23520  ptbasfi  23524  txbasval  23549  ptpjopn  23555  ptclsg  23558  dfac14lem  23560  xkoccn  23562  txcnp  23563  ptcnplem  23564  ptcnp  23565  txtube  23583  txcmplem1  23584  txcmplem2  23585  tx2ndc  23594  txkgen  23595  xkoco1cn  23600  xkoco2cn  23601  xkococnlem  23602  xkococn  23603  xkoinjcn  23630  qtoprest  23660  kqsat  23674  kqcldsat  23676  isfild  23801  fbunfip  23812  fgabs  23822  filconn  23826  fbasrn  23827  filufint  23863  elfm2  23891  elfm3  23893  fmfnfm  23901  hausflimi  23923  cnpflfi  23942  ptcmplem2  23996  tmdgsum2  24039  cldsubg  24054  qustgpopn  24063  ustfilxp  24156  bldisj  24342  xbln0  24358  blssps  24368  blss  24369  blssexps  24370  blssex  24371  blcls  24450  metcnp3  24484  icccmplem2  24768  mpomulcn  24814  cnheibor  24910  iscau4  25236  cmssmscld  25307  ovolshftlem2  25468  ovolicc2lem5  25479  dyadmax  25556  mbfi1fseqlem4  25676  mbfi1flimlem  25680  lhop1lem  25975  dvfsumrlim  25995  aalioulem3  26299  ulmcn  26365  radcnvlt1  26384  pilem2  26419  efopn  26624  cxpeq0  26644  cxpmul2z  26657  cxpcn3lem  26714  xrlimcnp  26935  vmappw  27083  fsumvma  27181  dchrptlem1  27232  lgsqr  27319  lgsdchrval  27322  2lgslem3  27372  2sqlem6  27391  2sqlem7  27392  2sqreultlem  27415  2sqreunnltlem  27418  pntlem3  27577  pntleml  27579  sltval2  27625  nosupno  27672  nosupbnd1lem5  27681  noinfno  27687  sletr  27727  madebdayim  27856  sltlpss  27876  negsid  28004  noseqinds  28244  brbtwn  28883  brcgr  28884  axcontlem8  28955  nbumgrvtx  29330  cusgrfilem2  29441  1loopgrnb0  29487  uspgr2wlkeq  29631  wlklenvclwlk  29640  upgrwlkdvdelem  29723  uspgrn2crct  29795  0enwwlksnge1  29851  usgr2wspthons3  29951  clwwlkccatlem  29975  clwlkclwwlkf  29994  clwwlknonel  30081  frgrncvvdeqlem9  30293  frgr2wwlkeqm  30317  frgrreggt1  30379  frgrreg  30380  pjhthmo  31288  spansncvi  31638  nmcexi  32012  cnlnssadj  32066  leopmuli  32119  elpjrn  32176  mdsl0  32296  sumdmdii  32401  fmptcof2  32640  suppss3  32706  lmxrge0  33988  bnj594  34948  bnj849  34961  subgrwlk  35159  erdszelem7  35224  sconnpi1  35266  cvmsval  35293  cvmopnlem  35305  cvmfolem  35306  cvmliftmolem2  35309  cvmlift2lem10  35339  cvmlift2lem12  35341  cvmlift3lem5  35350  cvmlift3lem8  35353  satfv0  35385  satfv1  35390  satfvsucsuc  35392  satffunlem1lem2  35430  satffunlem2lem2  35433  linethru  36176  opnrebl2  36344  neibastop2lem  36383  neibastop2  36384  bj-cbv3ta  36809  isinf2  37428  phpreu  37633  finixpnum  37634  lindsadd  37642  matunitlindflem1  37645  ptrecube  37649  poimirlem26  37675  poimirlem27  37676  poimirlem31  37680  poimir  37682  heicant  37684  voliunnfl  37693  volsupnfl  37694  itg2addnclem  37700  unirep  37743  sdclem2  37771  istotbnd3  37800  ssbnd  37817  eldisjlem19  38833  lshpdisj  39010  lsatn0  39022  lsat0cv  39056  cvrletrN  39296  cvrval4N  39438  lncvrelatN  39805  paddasslem14  39857  paddasslem15  39858  paddasslem16  39859  pmapjoin  39876  dihglblem2N  41318  dochvalr  41381  eqresfnbd  42250  sn-sup2  42489  prjspner1  42624  flt4lem7  42657  incssnn0  42709  eldioph4b  42809  diophren  42811  fphpdo  42815  rencldnfilem  42818  pellexlem5  42831  pell1234qrne0  42851  pell1234qrmulcl  42853  pell14qrgt0  42857  pell1234qrdich  42859  pell14qrdich  42867  pell1qrge1  42868  pell1qrgap  42872  pellfundre  42879  pellfundlb  42882  dvdsacongtr  42983  jm2.19lem4  42991  aomclem4  43056  hbtlem2  43123  hbtlem4  43125  hbtlem6  43128  cantnfresb  43323  dflim5  43328  tfsconcatrn  43341  tfsconcatrev  43347  naddwordnexlem4  43400  safesnsupfiss  43414  harval3  43537  clcnvlem  43622  ordpss  44450  relpfrlem  44953  cfsetsnfsetfo  47069  euoreqb  47118  2reu8i  47122  sprsymrelf1lem  47485  sprsymrelfolem2  47487  reupr  47516  fmtnofac2lem  47562  opoeALTV  47677  opeoALTV  47678  fpprwpprb  47734  gboge9  47758  clnbgrel  47822  grimco  47882  uhgrimedgi  47883  isuspgrim  47889  cycldlenngric  47921  uhgrimisgrgric  47924  clnbgrgrimlem  47926  clnbgrgrim  47927  grtriprop  47933  stgrusgra  47951  grlictr  48000  gpgcubic  48061  gpg5nbgr3star  48063  ellcoellss  48391  nn0sumshdiglem1  48581  itschlc0xyqsol  48727  itsclc0  48731  opnneilv  48863