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  5083  reusv3  5347  euotd  5458  swopo  5540  sotr3  5570  wereu2  5618  poirr2  6078  sossfld  6141  reuop  6248  frpomin  6295  oneqmini  6367  suctr  6402  elpreima  7000  fmptco  7071  isofrlem  7283  onmindif2  7749  resf1extb  7873  mptcnfimad  7927  frxp  8065  fnse  8072  suppss  8133  tposfo2  8188  wfr3g  8258  tz7.48-2  8370  omeulem1  8506  omeu  8509  nnaordex  8562  eldifsucnn  8588  pssnn  9088  onomeneq  9133  fodomfib  9223  fodomfibOLD  9225  dffi3  9325  supmo  9346  supnub  9356  infglb  9385  infnlb  9387  infmo  9391  infsupprpr  9400  cantnfle  9571  cantnflem1  9589  epfrs  9631  frr3g  9659  updjud  9837  alephord2i  9978  cardinfima  9998  aceq3lem  10021  dfac2b  10032  dfac12lem2  10046  axdc2lem  10349  ttukeylem6  10415  alephval2  10473  fpwwe2lem11  10542  fpwwe2lem12  10543  prlem934  10934  reclem4pr  10951  suplem1pr  10953  letr  11217  sup2  12088  uzind  12575  ledivge1le  12973  xrletr  13067  xltnegi  13125  xlemul1a  13197  ixxssixx  13269  difreicc  13394  flval3  13729  fsequb  13892  seqf1olem1  13958  expnegz  14013  hash2prd  14392  ccatrcl1  14512  relexprelg  14955  shftlem  14985  rexuzre  15270  cau3lem  15272  caubnd2  15275  caubnd  15276  climrlim2  15464  climuni  15469  2clim  15489  o1co  15503  rlimno1  15571  climbdd  15589  caurcvg  15594  summolem2  15633  summo  15634  zsum  15635  fsumf1o  15640  fsumss  15642  fsumcl2lem  15648  fsumadd  15657  fsummulc2  15701  fsumconst  15707  fsumrelem  15724  prodmolem2  15852  prodmo  15853  zprod  15854  fprodf1o  15863  fprodss  15865  fprodcl2lem  15867  fprodmul  15877  fproddiv  15878  fprodconst  15895  fprodn0  15896  dfgcd2  16467  lcmfunsnlem2  16561  coprmproddvdslem  16583  cncongrprm  16650  prmpwdvds  16826  infpnlem1  16832  1arith  16849  vdwapun  16896  vdwlem11  16913  vdwnnlem2  16918  ramz  16947  ramcl  16951  prmlem0  17027  firest  17346  catpropd  17625  initoid  17918  termoid  17919  initoeu2lem1  17931  pltnle  18252  pltletr  18257  pospo  18259  psss  18496  isgrpid2  18899  f1omvdco2  19370  pgpfi  19527  frgpnabllem1  19795  gsumval3eu  19826  gsumzres  19831  gsumzcl2  19832  gsumzf1o  19834  gsumzaddlem  19843  gsumconst  19856  gsumzmhm  19859  gsumzoppg  19866  ablfaclem3  20011  dvdsrtr  20296  dvdsrmul1  20297  unitgrp  20311  domnmuln0  20634  lspsolvlem  21089  gsumfsum  21381  nzerooringczr  21427  obslbs  21677  gsummoncoe1  22233  pf1ind  22280  dmatscmcl  22428  scmatmulcl  22443  smatvscl  22449  mdetdiaglem  22523  cpmatinvcl  22642  mp2pm2mplem4  22734  cpmadugsumlemF  22801  eltg3  22887  tgidm  22905  neindisj  23042  tgrest  23084  restcld  23097  tgcn  23177  lmcnp  23229  iunconnlem  23352  2ndcredom  23375  2ndc1stc  23376  1stcrest  23378  2ndcrest  23379  2ndcdisj  23381  nllyrest  23411  nllyidm  23414  lfinpfin  23449  locfincmp  23451  ptpjpre1  23496  ptuni2  23501  ptbasin  23502  ptbasfi  23506  txbasval  23531  ptpjopn  23537  ptclsg  23540  dfac14lem  23542  xkoccn  23544  txcnp  23545  ptcnplem  23546  ptcnp  23547  txtube  23565  txcmplem1  23566  txcmplem2  23567  tx2ndc  23576  txkgen  23577  xkoco1cn  23582  xkoco2cn  23583  xkococnlem  23584  xkococn  23585  xkoinjcn  23612  qtoprest  23642  kqsat  23656  kqcldsat  23658  isfild  23783  fbunfip  23794  fgabs  23804  filconn  23808  fbasrn  23809  filufint  23845  elfm2  23873  elfm3  23875  fmfnfm  23883  hausflimi  23905  cnpflfi  23924  ptcmplem2  23978  tmdgsum2  24021  cldsubg  24036  qustgpopn  24045  ustfilxp  24138  bldisj  24323  xbln0  24339  blssps  24349  blss  24350  blssexps  24351  blssex  24352  blcls  24431  metcnp3  24465  icccmplem2  24749  mpomulcn  24795  cnheibor  24891  iscau4  25216  cmssmscld  25287  ovolshftlem2  25448  ovolicc2lem5  25459  dyadmax  25536  mbfi1fseqlem4  25656  mbfi1flimlem  25660  lhop1lem  25955  dvfsumrlim  25975  aalioulem3  26279  ulmcn  26345  radcnvlt1  26364  pilem2  26399  efopn  26604  cxpeq0  26624  cxpmul2z  26637  cxpcn3lem  26694  xrlimcnp  26915  vmappw  27063  fsumvma  27161  dchrptlem1  27212  lgsqr  27299  lgsdchrval  27302  2lgslem3  27352  2sqlem6  27371  2sqlem7  27372  2sqreultlem  27395  2sqreunnltlem  27398  pntlem3  27557  pntleml  27559  sltval2  27605  nosupno  27652  nosupbnd1lem5  27661  noinfno  27667  sletr  27707  madebdayim  27843  sltlpss  27863  negsid  27993  noseqinds  28233  brbtwn  28888  brcgr  28889  axcontlem8  28960  nbumgrvtx  29335  cusgrfilem2  29446  1loopgrnb0  29492  uspgr2wlkeq  29635  wlklenvclwlk  29643  upgrwlkdvdelem  29725  uspgrn2crct  29797  0enwwlksnge1  29853  usgr2wspthons3  29956  clwwlkccatlem  29980  clwlkclwwlkf  29999  clwwlknonel  30086  frgrncvvdeqlem9  30298  frgr2wwlkeqm  30322  frgrreggt1  30384  frgrreg  30385  pjhthmo  31293  spansncvi  31643  nmcexi  32017  cnlnssadj  32071  leopmuli  32124  elpjrn  32181  mdsl0  32301  sumdmdii  32406  fmptcof2  32650  suppss3  32717  lmxrge0  33976  bnj594  34935  bnj849  34948  subgrwlk  35187  erdszelem7  35252  sconnpi1  35294  cvmsval  35321  cvmopnlem  35333  cvmfolem  35334  cvmliftmolem2  35337  cvmlift2lem10  35367  cvmlift2lem12  35369  cvmlift3lem5  35378  cvmlift3lem8  35381  satfv0  35413  satfv1  35418  satfvsucsuc  35420  satffunlem1lem2  35458  satffunlem2lem2  35461  linethru  36208  opnrebl2  36376  neibastop2lem  36415  neibastop2  36416  bj-cbv3ta  36841  isinf2  37460  phpreu  37654  finixpnum  37655  lindsadd  37663  matunitlindflem1  37666  ptrecube  37670  poimirlem26  37696  poimirlem27  37697  poimirlem31  37701  poimir  37703  heicant  37705  voliunnfl  37714  volsupnfl  37715  itg2addnclem  37721  unirep  37764  sdclem2  37792  istotbnd3  37821  ssbnd  37838  eldisjlem19  38918  lshpdisj  39096  lsatn0  39108  lsat0cv  39142  cvrletrN  39382  cvrval4N  39523  lncvrelatN  39890  paddasslem14  39942  paddasslem15  39943  paddasslem16  39944  pmapjoin  39961  dihglblem2N  41403  dochvalr  41466  eqresfnbd  42340  sn-sup2  42599  prjspner1  42734  flt4lem7  42767  incssnn0  42818  eldioph4b  42918  diophren  42920  fphpdo  42924  rencldnfilem  42927  pellexlem5  42940  pell1234qrne0  42960  pell1234qrmulcl  42962  pell14qrgt0  42966  pell1234qrdich  42968  pell14qrdich  42976  pell1qrge1  42977  pell1qrgap  42981  pellfundre  42988  pellfundlb  42991  dvdsacongtr  43091  jm2.19lem4  43099  aomclem4  43164  hbtlem2  43231  hbtlem4  43233  hbtlem6  43236  cantnfresb  43431  dflim5  43436  tfsconcatrn  43449  tfsconcatrev  43455  naddwordnexlem4  43508  safesnsupfiss  43522  harval3  43645  clcnvlem  43730  ordpss  44557  relpfrlem  45060  cfsetsnfsetfo  47174  euoreqb  47223  2reu8i  47227  sprsymrelf1lem  47605  sprsymrelfolem2  47607  reupr  47636  fmtnofac2lem  47682  opoeALTV  47797  opeoALTV  47798  fpprwpprb  47854  gboge9  47878  clnbgrel  47942  grimco  48003  uhgrimedgi  48004  isuspgrim  48010  cycldlenngric  48042  uhgrimisgrgric  48045  clnbgrgrimlem  48047  clnbgrgrim  48048  grtriprop  48055  stgrusgra  48073  grlimedgclnbgr  48109  grlimprclnbgrvtx  48113  grlimgredgex  48114  grlictr  48129  gpgedg2iv  48181  gpgcubic  48193  gpg5nbgr3star  48195  pgnbgreunbgrlem2  48231  pgnbgreunbgrlem5  48237  ellcoellss  48550  nn0sumshdiglem1  48736  itschlc0xyqsol  48882  itsclc0  48886  opnneilv  49023