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  1070  3impia  1126  ralrimdva  3156  disjiun  5082  reusv3  5356  euotd  5476  swopo  5559  sotr3  5589  wereu2  5637  poirr2  6101  sossfld  6161  reuop  6269  frpomin  6316  oneqmini  6388  suctr  6423  elpreima  7028  fmptco  7100  isofrlem  7313  onmindif2  7779  resf1extb  7904  mptcnfimad  7956  frxp  8094  fnse  8101  suppss  8162  tposfo2  8217  wfr3g  8288  tz7.48-2  8401  omeulem1  8539  omeu  8542  nnaordex  8596  eldifsucnn  8622  pssnn  9126  onomeneq  9171  fodomfib  9262  fodomfibOLD  9264  dffi3  9367  supmo  9388  supnub  9398  infglb  9427  infnlb  9429  infmo  9433  infsupprpr  9442  cantnfle  9616  cantnflem1  9634  epfrs  9676  frr3g  9704  updjud  9882  alephord2i  10023  cardinfima  10043  aceq3lem  10066  dfac2b  10077  dfac12lem2  10091  axdc2lem  10395  ttukeylem6  10461  alephval2  10520  fpwwe2lem11  10589  fpwwe2lem12  10590  prlem934  10981  reclem4pr  10998  suplem1pr  11000  letr  11267  sup2  12138  uzind  12655  ledivge1le  13056  xrletr  13150  xltnegi  13209  xlemul1a  13281  ixxssixx  13353  difreicc  13478  flval3  13815  fsequb  13978  seqf1olem1  14044  expnegz  14099  hash2prd  14478  ccatrcl1  14598  relexprelg  15041  shftlem  15071  rexuzre  15356  cau3lem  15358  caubnd2  15361  caubnd  15362  climrlim2  15550  climuni  15555  2clim  15575  o1co  15589  rlimno1  15657  climbdd  15675  caurcvg  15680  summolem2  15719  summo  15720  zsum  15721  fsumf1o  15726  fsumss  15728  fsumcl2lem  15734  fsumadd  15743  fsummulc2  15787  fsumconst  15793  fsumrelem  15811  prodmolem2  15941  prodmo  15942  zprod  15943  fprodf1o  15952  fprodss  15954  fprodcl2lem  15956  fprodmul  15966  fproddiv  15967  fprodconst  15984  fprodn0  15985  dfgcd2  16556  lcmfunsnlem2  16650  coprmproddvdslem  16672  cncongrprm  16740  prmpwdvds  16916  infpnlem1  16922  1arith  16939  vdwapun  16986  vdwlem11  17003  vdwnnlem2  17008  ramz  17037  ramcl  17041  prmlem0  17117  firest  17437  catpropd  17717  initoid  18010  termoid  18011  initoeu2lem1  18023  pltnle  18344  pltletr  18349  pospo  18351  psss  18588  isgrpid2  18994  f1omvdco2  19464  pgpfi  19621  frgpnabllem1  19889  gsumval3eu  19920  gsumzres  19925  gsumzcl2  19926  gsumzf1o  19928  gsumzaddlem  19937  gsumconst  19950  gsumzmhm  19953  gsumzoppg  19960  ablfaclem3  20105  dvdsrtr  20389  dvdsrmul1  20390  unitgrp  20404  domnmuln0  20731  lspsolvlem  21185  gsumfsum  21459  nzerooringczr  21505  obslbs  21755  gsummoncoe1  22344  pf1ind  22391  dmatscmcl  22536  scmatmulcl  22551  smatvscl  22557  mdetdiaglem  22631  cpmatinvcl  22750  mp2pm2mplem4  22842  cpmadugsumlemF  22909  eltg3  22995  tgidm  23013  neindisj  23150  tgrest  23192  restcld  23205  tgcn  23285  lmcnp  23337  iunconnlem  23460  2ndcredom  23483  2ndc1stc  23484  1stcrest  23486  2ndcrest  23487  2ndcdisj  23489  nllyrest  23519  nllyidm  23522  lfinpfin  23557  locfincmp  23559  ptpjpre1  23604  ptuni2  23609  ptbasin  23610  ptbasfi  23614  txbasval  23639  ptpjopn  23645  ptclsg  23648  dfac14lem  23650  xkoccn  23652  txcnp  23653  ptcnplem  23654  ptcnp  23655  txtube  23673  txcmplem1  23674  txcmplem2  23675  tx2ndc  23684  txkgen  23685  xkoco1cn  23690  xkoco2cn  23691  xkococnlem  23692  xkococn  23693  xkoinjcn  23720  qtoprest  23750  kqsat  23764  kqcldsat  23766  isfild  23891  fbunfip  23902  fgabs  23912  filconn  23916  fbasrn  23917  filufint  23953  elfm2  23981  elfm3  23983  fmfnfm  23991  hausflimi  24013  cnpflfi  24032  ptcmplem2  24086  tmdgsum2  24129  cldsubg  24144  qustgpopn  24153  ustfilxp  24246  bldisj  24431  xbln0  24447  blssps  24457  blss  24458  blssexps  24459  blssex  24460  blcls  24539  metcnp3  24573  icccmplem2  24857  mpomulcn  24902  cnheibor  24990  iscau4  25314  cmssmscld  25385  ovolshftlem2  25545  ovolicc2lem5  25556  dyadmax  25633  mbfi1fseqlem4  25753  mbfi1flimlem  25757  lhop1lem  26048  dvfsumrlim  26066  aalioulem3  26368  ulmcn  26432  radcnvlt1  26451  pilem2  26485  efopn  26693  cxpeq0  26713  cxpmul2z  26726  cxpcn3lem  26782  xrlimcnp  27003  vmappw  27150  fsumvma  27247  dchrptlem1  27298  lgsqr  27385  lgsdchrval  27388  2lgslem3  27438  2sqlem6  27457  2sqlem7  27458  2sqreultlem  27481  2sqreunnltlem  27484  pntlem3  27643  pntleml  27645  ltsval2  27690  nosupno  27737  nosupbnd1lem5  27746  noinfno  27752  lestr  27796  madebdayim  27951  ltslpss  27971  negsid  28104  noseqinds  28356  brbtwn  29039  brcgr  29040  axcontlem8  29111  nbumgrvtx  29486  cusgrfilem2  29596  1loopgrnb0  29642  uspgr2wlkeq  29785  wlklenvclwlk  29793  upgrwlkdvdelem  29875  uspgrn2crct  29947  0enwwlksnge1  30003  usgr2wspthons3  30106  clwwlkccatlem  30130  clwlkclwwlkf  30149  clwwlknonel  30236  frgrncvvdeqlem9  30448  frgr2wwlkeqm  30472  frgrreggt1  30534  frgrreg  30535  pjhthmo  31444  spansncvi  31794  nmcexi  32168  cnlnssadj  32222  leopmuli  32275  elpjrn  32332  mdsl0  32452  sumdmdii  32557  fmptcof2  32802  suppss3  32868  lmxrge0  34203  bnj594  35164  bnj849  35177  noinfepfnregs  35383  subgrwlk  35430  erdszelem7  35495  sconnpi1  35537  cvmsval  35564  cvmopnlem  35576  cvmfolem  35577  cvmliftmolem2  35580  cvmlift2lem10  35610  cvmlift2lem12  35612  cvmlift3lem5  35621  cvmlift3lem8  35624  satfv0  35656  satfv1  35661  satfvsucsuc  35663  satffunlem1lem2  35701  satffunlem2lem2  35704  linethru  36451  opnrebl2  36629  neibastop2lem  36668  neibastop2  36669  bj-cbv3ta  37219  cgsex2gd  37577  isinf2  37847  phpreu  38051  finixpnum  38052  lindsadd  38060  matunitlindflem1  38063  ptrecube  38067  poimirlem26  38093  poimirlem27  38094  poimirlem31  38098  poimir  38100  heicant  38102  voliunnfl  38111  volsupnfl  38112  itg2addnclem  38118  unirep  38161  sdclem2  38189  istotbnd3  38218  ssbnd  38235  eldisjlem19  39360  lshpdisj  39559  lsatn0  39571  lsat0cv  39605  cvrletrN  39845  cvrval4N  39986  lncvrelatN  40353  paddasslem14  40405  paddasslem15  40406  paddasslem16  40407  pmapjoin  40424  dihglblem2N  41866  dochvalr  41929  eqresfnbd  42799  sn-sup2  43061  prjspner1  43156  flt4lem7  43189  incssnn0  43240  eldioph4b  43336  diophren  43338  fphpdo  43342  rencldnfilem  43345  pellexlem5  43358  pell1234qrne0  43378  pell1234qrmulcl  43380  pell14qrgt0  43384  pell1234qrdich  43386  pell14qrdich  43394  pell1qrge1  43395  pell1qrgap  43399  pellfundre  43406  pellfundlb  43409  dvdsacongtr  43509  jm2.19lem4  43517  aomclem4  43582  hbtlem2  43649  hbtlem4  43651  hbtlem6  43654  cantnfresb  43849  dflim5  43854  tfsconcatrn  43867  tfsconcatrev  43873  naddwordnexlem4  43926  safesnsupfiss  43939  harval3  44062  clcnvlem  44147  ordpss  44974  relpfrlem  45477  cfsetsnfsetfo  47602  euoreqb  47651  2reu8i  47655  sprsymrelf1lem  48045  sprsymrelfolem2  48047  reupr  48076  fmtnofac2lem  48125  opoeALTV  48253  opeoALTV  48254  fpprwpprb  48310  gboge9  48334  clnbgrel  48398  grimco  48459  uhgrimedgi  48460  isuspgrim  48466  cycldlenngric  48498  uhgrimisgrgric  48501  clnbgrgrimlem  48503  clnbgrgrim  48504  grtriprop  48511  stgrusgra  48529  grlimedgclnbgr  48565  grlimprclnbgrvtx  48569  grlimgredgex  48570  grlictr  48585  gpgedg2iv  48637  gpgcubic  48649  gpg5nbgr3star  48651  pgnbgreunbgrlem2  48687  pgnbgreunbgrlem5  48693  ellcoellss  49005  nn0sumshdiglem1  49191  itschlc0xyqsol  49337  itsclc0  49341  opnneilv  49478