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  1062  3impia  1118  ralrimdva  3137  disjiun  5087  reusv3  5351  euotd  5462  swopo  5544  sotr3  5574  wereu2  5622  poirr2  6082  sossfld  6145  reuop  6252  frpomin  6299  oneqmini  6371  suctr  6406  elpreima  7005  fmptco  7076  isofrlem  7288  onmindif2  7754  resf1extb  7878  mptcnfimad  7932  frxp  8070  fnse  8077  suppss  8138  tposfo2  8193  wfr3g  8263  tz7.48-2  8375  omeulem1  8511  omeu  8514  nnaordex  8568  eldifsucnn  8594  pssnn  9097  onomeneq  9142  fodomfib  9233  fodomfibOLD  9235  dffi3  9338  supmo  9359  supnub  9369  infglb  9398  infnlb  9400  infmo  9404  infsupprpr  9413  cantnfle  9584  cantnflem1  9602  epfrs  9644  frr3g  9672  updjud  9850  alephord2i  9991  cardinfima  10011  aceq3lem  10034  dfac2b  10045  dfac12lem2  10059  axdc2lem  10362  ttukeylem6  10428  alephval2  10487  fpwwe2lem11  10556  fpwwe2lem12  10557  prlem934  10948  reclem4pr  10965  suplem1pr  10967  letr  11231  sup2  12102  uzind  12588  ledivge1le  12982  xrletr  13076  xltnegi  13135  xlemul1a  13207  ixxssixx  13279  difreicc  13404  flval3  13739  fsequb  13902  seqf1olem1  13968  expnegz  14023  hash2prd  14402  ccatrcl1  14522  relexprelg  14965  shftlem  14995  rexuzre  15280  cau3lem  15282  caubnd2  15285  caubnd  15286  climrlim2  15474  climuni  15479  2clim  15499  o1co  15513  rlimno1  15581  climbdd  15599  caurcvg  15604  summolem2  15643  summo  15644  zsum  15645  fsumf1o  15650  fsumss  15652  fsumcl2lem  15658  fsumadd  15667  fsummulc2  15711  fsumconst  15717  fsumrelem  15734  prodmolem2  15862  prodmo  15863  zprod  15864  fprodf1o  15873  fprodss  15875  fprodcl2lem  15877  fprodmul  15887  fproddiv  15888  fprodconst  15905  fprodn0  15906  dfgcd2  16477  lcmfunsnlem2  16571  coprmproddvdslem  16593  cncongrprm  16660  prmpwdvds  16836  infpnlem1  16842  1arith  16859  vdwapun  16906  vdwlem11  16923  vdwnnlem2  16928  ramz  16957  ramcl  16961  prmlem0  17037  firest  17356  catpropd  17636  initoid  17929  termoid  17930  initoeu2lem1  17942  pltnle  18263  pltletr  18268  pospo  18270  psss  18507  isgrpid2  18910  f1omvdco2  19381  pgpfi  19538  frgpnabllem1  19806  gsumval3eu  19837  gsumzres  19842  gsumzcl2  19843  gsumzf1o  19845  gsumzaddlem  19854  gsumconst  19867  gsumzmhm  19870  gsumzoppg  19877  ablfaclem3  20022  dvdsrtr  20308  dvdsrmul1  20309  unitgrp  20323  domnmuln0  20646  lspsolvlem  21101  gsumfsum  21393  nzerooringczr  21439  obslbs  21689  gsummoncoe1  22256  pf1ind  22303  dmatscmcl  22451  scmatmulcl  22466  smatvscl  22472  mdetdiaglem  22546  cpmatinvcl  22665  mp2pm2mplem4  22757  cpmadugsumlemF  22824  eltg3  22910  tgidm  22928  neindisj  23065  tgrest  23107  restcld  23120  tgcn  23200  lmcnp  23252  iunconnlem  23375  2ndcredom  23398  2ndc1stc  23399  1stcrest  23401  2ndcrest  23402  2ndcdisj  23404  nllyrest  23434  nllyidm  23437  lfinpfin  23472  locfincmp  23474  ptpjpre1  23519  ptuni2  23524  ptbasin  23525  ptbasfi  23529  txbasval  23554  ptpjopn  23560  ptclsg  23563  dfac14lem  23565  xkoccn  23567  txcnp  23568  ptcnplem  23569  ptcnp  23570  txtube  23588  txcmplem1  23589  txcmplem2  23590  tx2ndc  23599  txkgen  23600  xkoco1cn  23605  xkoco2cn  23606  xkococnlem  23607  xkococn  23608  xkoinjcn  23635  qtoprest  23665  kqsat  23679  kqcldsat  23681  isfild  23806  fbunfip  23817  fgabs  23827  filconn  23831  fbasrn  23832  filufint  23868  elfm2  23896  elfm3  23898  fmfnfm  23906  hausflimi  23928  cnpflfi  23947  ptcmplem2  24001  tmdgsum2  24044  cldsubg  24059  qustgpopn  24068  ustfilxp  24161  bldisj  24346  xbln0  24362  blssps  24372  blss  24373  blssexps  24374  blssex  24375  blcls  24454  metcnp3  24488  icccmplem2  24772  mpomulcn  24818  cnheibor  24914  iscau4  25239  cmssmscld  25310  ovolshftlem2  25471  ovolicc2lem5  25482  dyadmax  25559  mbfi1fseqlem4  25679  mbfi1flimlem  25683  lhop1lem  25978  dvfsumrlim  25998  aalioulem3  26302  ulmcn  26368  radcnvlt1  26387  pilem2  26422  efopn  26627  cxpeq0  26647  cxpmul2z  26660  cxpcn3lem  26717  xrlimcnp  26938  vmappw  27086  fsumvma  27184  dchrptlem1  27235  lgsqr  27322  lgsdchrval  27325  2lgslem3  27375  2sqlem6  27394  2sqlem7  27395  2sqreultlem  27418  2sqreunnltlem  27421  pntlem3  27580  pntleml  27582  sltval2  27628  nosupno  27675  nosupbnd1lem5  27684  noinfno  27690  sletr  27734  madebdayim  27870  sltlpss  27890  negsid  28023  noseqinds  28274  brbtwn  28955  brcgr  28956  axcontlem8  29027  nbumgrvtx  29402  cusgrfilem2  29513  1loopgrnb0  29559  uspgr2wlkeq  29702  wlklenvclwlk  29710  upgrwlkdvdelem  29792  uspgrn2crct  29864  0enwwlksnge1  29920  usgr2wspthons3  30023  clwwlkccatlem  30047  clwlkclwwlkf  30066  clwwlknonel  30153  frgrncvvdeqlem9  30365  frgr2wwlkeqm  30389  frgrreggt1  30451  frgrreg  30452  pjhthmo  31360  spansncvi  31710  nmcexi  32084  cnlnssadj  32138  leopmuli  32191  elpjrn  32248  mdsl0  32368  sumdmdii  32473  fmptcof2  32717  suppss3  32783  lmxrge0  34090  bnj594  35049  bnj849  35062  noinfepfnregs  35269  subgrwlk  35307  erdszelem7  35372  sconnpi1  35414  cvmsval  35441  cvmopnlem  35453  cvmfolem  35454  cvmliftmolem2  35457  cvmlift2lem10  35487  cvmlift2lem12  35489  cvmlift3lem5  35498  cvmlift3lem8  35501  satfv0  35533  satfv1  35538  satfvsucsuc  35540  satffunlem1lem2  35578  satffunlem2lem2  35581  linethru  36328  opnrebl2  36496  neibastop2lem  36535  neibastop2  36536  bj-cbv3ta  36962  isinf2  37581  phpreu  37776  finixpnum  37777  lindsadd  37785  matunitlindflem1  37788  ptrecube  37792  poimirlem26  37818  poimirlem27  37819  poimirlem31  37823  poimir  37825  heicant  37827  voliunnfl  37836  volsupnfl  37837  itg2addnclem  37843  unirep  37886  sdclem2  37914  istotbnd3  37943  ssbnd  37960  eldisjlem19  39085  lshpdisj  39284  lsatn0  39296  lsat0cv  39330  cvrletrN  39570  cvrval4N  39711  lncvrelatN  40078  paddasslem14  40130  paddasslem15  40131  paddasslem16  40132  pmapjoin  40149  dihglblem2N  41591  dochvalr  41654  eqresfnbd  42525  sn-sup2  42782  prjspner1  42905  flt4lem7  42938  incssnn0  42989  eldioph4b  43089  diophren  43091  fphpdo  43095  rencldnfilem  43098  pellexlem5  43111  pell1234qrne0  43131  pell1234qrmulcl  43133  pell14qrgt0  43137  pell1234qrdich  43139  pell14qrdich  43147  pell1qrge1  43148  pell1qrgap  43152  pellfundre  43159  pellfundlb  43162  dvdsacongtr  43262  jm2.19lem4  43270  aomclem4  43335  hbtlem2  43402  hbtlem4  43404  hbtlem6  43407  cantnfresb  43602  dflim5  43607  tfsconcatrn  43620  tfsconcatrev  43626  naddwordnexlem4  43679  safesnsupfiss  43692  harval3  43815  clcnvlem  43900  ordpss  44727  relpfrlem  45230  cfsetsnfsetfo  47342  euoreqb  47391  2reu8i  47395  sprsymrelf1lem  47773  sprsymrelfolem2  47775  reupr  47804  fmtnofac2lem  47850  opoeALTV  47965  opeoALTV  47966  fpprwpprb  48022  gboge9  48046  clnbgrel  48110  grimco  48171  uhgrimedgi  48172  isuspgrim  48178  cycldlenngric  48210  uhgrimisgrgric  48213  clnbgrgrimlem  48215  clnbgrgrim  48216  grtriprop  48223  stgrusgra  48241  grlimedgclnbgr  48277  grlimprclnbgrvtx  48281  grlimgredgex  48282  grlictr  48297  gpgedg2iv  48349  gpgcubic  48361  gpg5nbgr3star  48363  pgnbgreunbgrlem2  48399  pgnbgreunbgrlem5  48405  ellcoellss  48717  nn0sumshdiglem1  48903  itschlc0xyqsol  49049  itsclc0  49053  opnneilv  49190