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  3129  disjiun  5083  reusv3  5347  euotd  5460  swopo  5542  sotr3  5572  wereu2  5620  poirr2  6077  sossfld  6139  reuop  6245  frpomin  6292  oneqmini  6364  suctr  6399  elpreima  6996  fmptco  7067  isofrlem  7281  onmindif2  7747  resf1extb  7874  mptcnfimad  7928  frxp  8066  fnse  8073  suppss  8134  tposfo2  8189  wfr3g  8259  tz7.48-2  8371  omeulem1  8507  omeu  8510  nnaordex  8563  eldifsucnn  8589  pssnn  9092  onomeneq  9138  fodomfib  9238  fodomfibOLD  9240  dffi3  9340  supmo  9361  supnub  9371  infglb  9400  infnlb  9402  infmo  9406  infsupprpr  9415  cantnfle  9586  cantnflem1  9604  epfrs  9646  frr3g  9671  updjud  9849  alephord2i  9990  cardinfima  10010  aceq3lem  10033  dfac2b  10044  dfac12lem2  10058  axdc2lem  10361  ttukeylem6  10427  alephval2  10485  fpwwe2lem11  10554  fpwwe2lem12  10555  prlem934  10946  reclem4pr  10963  suplem1pr  10965  letr  11228  sup2  12099  uzind  12586  ledivge1le  12984  xrletr  13078  xltnegi  13136  xlemul1a  13208  ixxssixx  13280  difreicc  13405  flval3  13737  fsequb  13900  seqf1olem1  13966  expnegz  14021  hash2prd  14400  ccatrcl1  14519  relexprelg  14963  shftlem  14993  rexuzre  15278  cau3lem  15280  caubnd2  15283  caubnd  15284  climrlim2  15472  climuni  15477  2clim  15497  o1co  15511  rlimno1  15579  climbdd  15597  caurcvg  15602  summolem2  15641  summo  15642  zsum  15643  fsumf1o  15648  fsumss  15650  fsumcl2lem  15656  fsumadd  15665  fsummulc2  15709  fsumconst  15715  fsumrelem  15732  prodmolem2  15860  prodmo  15861  zprod  15862  fprodf1o  15871  fprodss  15873  fprodcl2lem  15875  fprodmul  15885  fproddiv  15886  fprodconst  15903  fprodn0  15904  dfgcd2  16475  lcmfunsnlem2  16569  coprmproddvdslem  16591  cncongrprm  16658  prmpwdvds  16834  infpnlem1  16840  1arith  16857  vdwapun  16904  vdwlem11  16921  vdwnnlem2  16926  ramz  16955  ramcl  16959  prmlem0  17035  firest  17354  catpropd  17633  initoid  17926  termoid  17927  initoeu2lem1  17939  pltnle  18260  pltletr  18265  pospo  18267  psss  18504  isgrpid2  18873  f1omvdco2  19345  pgpfi  19502  frgpnabllem1  19770  gsumval3eu  19801  gsumzres  19806  gsumzcl2  19807  gsumzf1o  19809  gsumzaddlem  19818  gsumconst  19831  gsumzmhm  19834  gsumzoppg  19841  ablfaclem3  19986  dvdsrtr  20271  dvdsrmul1  20272  unitgrp  20286  domnmuln0  20612  lspsolvlem  21067  gsumfsum  21359  nzerooringczr  21405  obslbs  21655  gsummoncoe1  22211  pf1ind  22258  dmatscmcl  22406  scmatmulcl  22421  smatvscl  22427  mdetdiaglem  22501  cpmatinvcl  22620  mp2pm2mplem4  22712  cpmadugsumlemF  22779  eltg3  22865  tgidm  22883  neindisj  23020  tgrest  23062  restcld  23075  tgcn  23155  lmcnp  23207  iunconnlem  23330  2ndcredom  23353  2ndc1stc  23354  1stcrest  23356  2ndcrest  23357  2ndcdisj  23359  nllyrest  23389  nllyidm  23392  lfinpfin  23427  locfincmp  23429  ptpjpre1  23474  ptuni2  23479  ptbasin  23480  ptbasfi  23484  txbasval  23509  ptpjopn  23515  ptclsg  23518  dfac14lem  23520  xkoccn  23522  txcnp  23523  ptcnplem  23524  ptcnp  23525  txtube  23543  txcmplem1  23544  txcmplem2  23545  tx2ndc  23554  txkgen  23555  xkoco1cn  23560  xkoco2cn  23561  xkococnlem  23562  xkococn  23563  xkoinjcn  23590  qtoprest  23620  kqsat  23634  kqcldsat  23636  isfild  23761  fbunfip  23772  fgabs  23782  filconn  23786  fbasrn  23787  filufint  23823  elfm2  23851  elfm3  23853  fmfnfm  23861  hausflimi  23883  cnpflfi  23902  ptcmplem2  23956  tmdgsum2  23999  cldsubg  24014  qustgpopn  24023  ustfilxp  24116  bldisj  24302  xbln0  24318  blssps  24328  blss  24329  blssexps  24330  blssex  24331  blcls  24410  metcnp3  24444  icccmplem2  24728  mpomulcn  24774  cnheibor  24870  iscau4  25195  cmssmscld  25266  ovolshftlem2  25427  ovolicc2lem5  25438  dyadmax  25515  mbfi1fseqlem4  25635  mbfi1flimlem  25639  lhop1lem  25934  dvfsumrlim  25954  aalioulem3  26258  ulmcn  26324  radcnvlt1  26343  pilem2  26378  efopn  26583  cxpeq0  26603  cxpmul2z  26616  cxpcn3lem  26673  xrlimcnp  26894  vmappw  27042  fsumvma  27140  dchrptlem1  27191  lgsqr  27278  lgsdchrval  27281  2lgslem3  27331  2sqlem6  27350  2sqlem7  27351  2sqreultlem  27374  2sqreunnltlem  27377  pntlem3  27536  pntleml  27538  sltval2  27584  nosupno  27631  nosupbnd1lem5  27640  noinfno  27646  sletr  27686  madebdayim  27820  sltlpss  27840  negsid  27970  noseqinds  28210  brbtwn  28862  brcgr  28863  axcontlem8  28934  nbumgrvtx  29309  cusgrfilem2  29420  1loopgrnb0  29466  uspgr2wlkeq  29609  wlklenvclwlk  29617  upgrwlkdvdelem  29699  uspgrn2crct  29771  0enwwlksnge1  29827  usgr2wspthons3  29927  clwwlkccatlem  29951  clwlkclwwlkf  29970  clwwlknonel  30057  frgrncvvdeqlem9  30269  frgr2wwlkeqm  30293  frgrreggt1  30355  frgrreg  30356  pjhthmo  31264  spansncvi  31614  nmcexi  31988  cnlnssadj  32042  leopmuli  32095  elpjrn  32152  mdsl0  32272  sumdmdii  32377  fmptcof2  32614  suppss3  32680  lmxrge0  33918  bnj594  34878  bnj849  34891  subgrwlk  35104  erdszelem7  35169  sconnpi1  35211  cvmsval  35238  cvmopnlem  35250  cvmfolem  35251  cvmliftmolem2  35254  cvmlift2lem10  35284  cvmlift2lem12  35286  cvmlift3lem5  35295  cvmlift3lem8  35298  satfv0  35330  satfv1  35335  satfvsucsuc  35337  satffunlem1lem2  35375  satffunlem2lem2  35378  linethru  36126  opnrebl2  36294  neibastop2lem  36333  neibastop2  36334  bj-cbv3ta  36759  isinf2  37378  phpreu  37583  finixpnum  37584  lindsadd  37592  matunitlindflem1  37595  ptrecube  37599  poimirlem26  37625  poimirlem27  37626  poimirlem31  37630  poimir  37632  heicant  37634  voliunnfl  37643  volsupnfl  37644  itg2addnclem  37650  unirep  37693  sdclem2  37721  istotbnd3  37750  ssbnd  37767  eldisjlem19  38787  lshpdisj  38965  lsatn0  38977  lsat0cv  39011  cvrletrN  39251  cvrval4N  39393  lncvrelatN  39760  paddasslem14  39812  paddasslem15  39813  paddasslem16  39814  pmapjoin  39831  dihglblem2N  41273  dochvalr  41336  eqresfnbd  42205  sn-sup2  42464  prjspner1  42599  flt4lem7  42632  incssnn0  42684  eldioph4b  42784  diophren  42786  fphpdo  42790  rencldnfilem  42793  pellexlem5  42806  pell1234qrne0  42826  pell1234qrmulcl  42828  pell14qrgt0  42832  pell1234qrdich  42834  pell14qrdich  42842  pell1qrge1  42843  pell1qrgap  42847  pellfundre  42854  pellfundlb  42857  dvdsacongtr  42957  jm2.19lem4  42965  aomclem4  43030  hbtlem2  43097  hbtlem4  43099  hbtlem6  43102  cantnfresb  43297  dflim5  43302  tfsconcatrn  43315  tfsconcatrev  43321  naddwordnexlem4  43374  safesnsupfiss  43388  harval3  43511  clcnvlem  43596  ordpss  44424  relpfrlem  44927  cfsetsnfsetfo  47045  euoreqb  47094  2reu8i  47098  sprsymrelf1lem  47476  sprsymrelfolem2  47478  reupr  47507  fmtnofac2lem  47553  opoeALTV  47668  opeoALTV  47669  fpprwpprb  47725  gboge9  47749  clnbgrel  47813  grimco  47873  uhgrimedgi  47874  isuspgrim  47880  cycldlenngric  47912  uhgrimisgrgric  47915  clnbgrgrimlem  47917  clnbgrgrim  47918  grtriprop  47924  stgrusgra  47942  grlictr  47991  gpgedg2iv  48042  gpgcubic  48054  gpg5nbgr3star  48056  pgnbgreunbgrlem2  48091  pgnbgreunbgrlem5  48097  ellcoellss  48408  nn0sumshdiglem1  48594  itschlc0xyqsol  48740  itsclc0  48744  opnneilv  48881