Theorem expimpd 458

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 417	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 415	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ornld  1075  3impia  1133  ralrimdva  3163  disjiun  5096  reusv3  5376  euotd  5496  swopo  5580  sotr3  5610  wereu2  5658  poirr2  6124  sossfld  6184  reuop  6294  frpomin  6341  ordpss  6389  oneqmini  6414  suctr  6449  elpreima  7053  fmptco  7125  isofrlem  7338  onmindif2  7805  resf1extb  7930  mptcnfimad  7982  frxp  8121  fnse  8128  suppss  8189  tposfo2  8244  wfr3g  8315  tz7.48-2  8428  omeulem1  8566  omeu  8569  nnaordex  8623  eldifsucnn  8649  pssnn  9152  onomeneq  9197  fodomfib  9287  dffi3  9390  supmo  9411  supnub  9421  infglb  9450  infnlb  9452  infmo  9456  infsupprpr  9465  cantnfle  9639  cantnflem1  9657  epfrs  9699  frr3g  9727  updjud  9919  alephord2i  10060  cardinfima  10080  aceq3lem  10103  dfac2b  10113  dfac12lem2  10127  axdc2lem  10431  ttukeylem6  10497  alephval2  10556  fpwwe2lem11  10625  fpwwe2lem12  10626  prlem934  11017  reclem4pr  11034  suplem1pr  11036  letr  11303  sup2  12170  uzind  12687  ledivge1le  13088  xrletr  13182  xltnegi  13241  xlemul1a  13313  ixxssixx  13385  difreicc  13510  flval3  13848  fsequb  14011  seqf1olem1  14077  expnegz  14132  hash2prd  14512  ccatrcl1  14632  relexprelg  15075  shftlem  15105  rexuzre  15404  cau3lem  15406  caubnd2  15409  caubnd  15410  climrlim2  15598  climuni  15603  2clim  15623  o1co  15637  rlimno1  15705  climbdd  15723  caurcvg  15728  summolem2  15767  summo  15768  zsum  15769  fsumf1o  15774  fsumss  15776  fsumcl2lem  15782  fsumadd  15791  fsummulc2  15835  fsumconst  15841  fsumrelem  15859  prodmolem2  15989  prodmo  15990  zprod  15991  fprodf1o  16000  fprodss  16002  fprodcl2lem  16004  fprodmul  16014  fproddiv  16015  fprodconst  16032  fprodn0  16033  dfgcd2  16603  lcmfunsnlem2  16697  coprmproddvdslem  16719  cncongrprm  16787  prmpwdvds  16963  infpnlem1  16969  1arith  16986  vdwapun  17033  vdwlem11  17050  vdwnnlem2  17055  ramz  17084  ramcl  17088  prmlem0  17164  firest  17484  catpropd  17764  initoid  18057  termoid  18058  initoeu2lem1  18070  pltnle  18391  pltletr  18396  pospo  18398  psss  18635  isgrpid2  19042  f1omvdco2  19517  pgpfi  19674  frgpnabllem1  19942  gsumval3eu  19973  gsumzres  19978  gsumzcl2  19979  gsumzf1o  19981  gsumzaddlem  19990  gsumconst  20003  gsumzmhm  20006  gsumzoppg  20013  ablfaclem3  20158  dvdsrtr  20449  dvdsrmul1  20450  unitgrp  20464  domnmuln0  20793  lspsolvlem  21245  gsumfsum  21563  nzerooringczr  21609  obslbs  21859  gsummoncoe1  22447  pf1ind  22494  dmatscmcl  22639  scmatmulcl  22654  smatvscl  22660  mdetdiaglem  22734  cpmatinvcl  22853  mp2pm2mplem4  22945  cpmadugsumlemF  23012  eltg3  23098  tgidm  23116  neindisj  23253  tgrest  23295  restcld  23308  tgcn  23388  lmcnp  23440  iunconnlem  23563  2ndcredom  23586  2ndc1stc  23587  1stcrest  23589  2ndcrest  23590  2ndcdisj  23592  nllyrest  23622  nllyidm  23625  lfinpfin  23660  locfincmp  23662  ptpjpre1  23707  ptuni2  23712  ptbasin  23713  ptbasfi  23717  txbasval  23742  ptpjopn  23748  ptclsg  23751  dfac14lem  23753  xkoccn  23755  txcnp  23756  ptcnplem  23757  ptcnp  23758  txtube  23776  txcmplem1  23777  txcmplem2  23778  tx2ndc  23787  txkgen  23788  xkoco1cn  23793  xkoco2cn  23794  xkococnlem  23795  xkococn  23796  xkoinjcn  23823  qtoprest  23853  kqsat  23867  kqcldsat  23869  isfild  23994  fbunfip  24005  fgabs  24015  filconn  24019  fbasrn  24020  filufint  24056  elfm2  24084  elfm3  24086  fmfnfm  24094  hausflimi  24116  cnpflfi  24135  ptcmplem2  24189  tmdgsum2  24232  cldsubg  24247  qustgpopn  24256  ustfilxp  24349  bldisj  24534  xbln0  24550  blssps  24560  blss  24561  blssexps  24562  blssex  24563  blcls  24642  metcnp3  24676  icccmplem2  24960  mpomulcn  25005  cnheibor  25093  iscau4  25417  cmssmscld  25488  ovolshftlem2  25648  ovolicc2lem5  25659  dyadmax  25736  mbfi1fseqlem4  25856  mbfi1flimlem  25860  lhop1lem  26151  dvfsumrlim  26169  aalioulem3  26474  ulmcn  26538  radcnvlt1  26557  pilem2  26591  efopn  26799  cxpeq0  26819  cxpmul2z  26832  cxpcn3lem  26888  xrlimcnp  27109  vmappw  27256  fsumvma  27353  dchrptlem1  27404  lgsqr  27491  lgsdchrval  27494  2lgslem3  27544  2sqlem6  27563  2sqlem7  27564  2sqreultlem  27587  2sqreunnltlem  27590  pntlem3  27749  pntleml  27751  ltsval2  27796  nosupno  27843  nosupbnd1lem5  27852  noinfno  27858  lestr  27902  madebdayim  28057  ltslpss  28077  negsid  28210  noseqinds  28462  brbtwn  29215  brcgr  29216  axcontlem8  29287  nbumgrvtx  29662  cusgrfilem2  29772  1loopgrnb0  29818  uspgr2wlkeq  29961  wlklenvclwlk  29969  upgrwlkdvdelem  30051  uspgrn2crct  30123  0enwwlksnge1  30179  usgr2wspthons3  30282  clwwlkccatlem  30306  clwlkclwwlkf  30325  clwwlknonel  30412  frgrncvvdeqlem9  30624  frgr2wwlkeqm  30648  frgrreggt1  30710  frgrreg  30711  pjhthmo  31620  spansncvi  31970  nmcexi  32344  cnlnssadj  32398  leopmuli  32451  elpjrn  32508  mdsl0  32628  sumdmdii  32733  fmptcof2  32968  suppss3  33034  lmxrge0  34308  bnj594  35266  bnj849  35279  noinfepfnregs  35511  subgrwlk  35590  erdszelem7  35655  sconnpi1  35697  cvmsval  35724  cvmopnlem  35736  cvmfolem  35737  cvmliftmolem2  35740  cvmlift2lem10  35770  cvmlift2lem12  35772  cvmlift3lem5  35781  cvmlift3lem8  35784  satfv0  35816  satfv1  35821  satfvsucsuc  35823  satffunlem1lem2  35861  satffunlem2lem2  35864  linethru  36611  opnrebl2  36798  neibastop2lem  36837  neibastop2  36838  bj-cbv3ta  37387  cgsex2gd  37747  isinf2  38017  phpreu  38221  finixpnum  38222  lindsadd  38230  matunitlindflem1  38233  ptrecube  38237  poimirlem26  38263  poimirlem27  38264  poimirlem31  38268  poimir  38270  heicant  38272  voliunnfl  38281  volsupnfl  38282  itg2addnclem  38288  unirep  38331  sdclem2  38359  istotbnd3  38388  ssbnd  38405  eldisjlem19  39530  lshpdisj  39729  lsatn0  39741  lsat0cv  39775  cvrletrN  40015  cvrval4N  40156  lncvrelatN  40523  paddasslem14  40575  paddasslem15  40576  paddasslem16  40577  pmapjoin  40594  dihglblem2N  42036  dochvalr  42099  eqresfnbd  42971  sn-sup2  43233  prjspner1  43328  flt4lem7  43361  incssnn0  43412  eldioph4b  43508  diophren  43510  fphpdo  43514  rencldnfilem  43517  pellexlem5  43530  pell1234qrne0  43550  pell1234qrmulcl  43552  pell14qrgt0  43556  pell1234qrdich  43558  pell14qrdich  43566  pell1qrge1  43567  pell1qrgap  43571  pellfundre  43578  pellfundlb  43581  dvdsacongtr  43681  jm2.19lem4  43689  aomclem4  43754  hbtlem2  43821  hbtlem4  43823  hbtlem6  43826  cantnfresb  44021  dflim5  44026  tfsconcatrn  44039  tfsconcatrev  44045  naddwordnexlem4  44098  safesnsupfiss  44111  harval3  44234  clcnvlem  44319  relpfrlem  45632  cfsetsnfsetfo  47764  euoreqb  47813  2reu8i  47817  sprsymrelf1lem  48207  sprsymrelfolem2  48209  reupr  48238  fmtnofac2lem  48287  opoeALTV  48415  opeoALTV  48416  fpprwpprb  48472  gboge9  48496  clnbgrel  48560  grimco  48621  uhgrimedgi  48622  isuspgrim  48628  cycldlenngric  48660  uhgrimisgrgric  48663  clnbgrgrimlem  48665  clnbgrgrim  48666  grtriprop  48673  stgrusgra  48691  grlimedgclnbgr  48727  grlimprclnbgrvtx  48731  grlimgredgex  48732  grlictr  48747  gpgedg2iv  48799  gpgcubic  48811  gpg5nbgr3star  48813  pgnbgreunbgrlem2  48849  pgnbgreunbgrlem5  48855  ellcoellss  49182  nn0sumshdiglem1  49368  itschlc0xyqsol  49514  itsclc0  49518  opnneilv  49654