Theorem expimpd 454

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ornld  1067  3impia  1123  ralrimdva  3140  disjiun  5067  reusv3  5341  euotd  5461  swopo  5544  sotr3  5574  wereu2  5622  poirr2  6081  sossfld  6144  reuop  6251  frpomin  6298  oneqmini  6370  suctr  6405  elpreima  7006  fmptco  7078  isofrlem  7291  onmindif2  7757  resf1extb  7881  mptcnfimad  7935  frxp  8073  fnse  8080  suppss  8141  tposfo2  8196  wfr3g  8266  tz7.48-2  8378  omeulem1  8514  omeu  8517  nnaordex  8571  eldifsucnn  8597  pssnn  9100  onomeneq  9145  fodomfib  9236  fodomfibOLD  9238  dffi3  9341  supmo  9362  supnub  9372  infglb  9401  infnlb  9403  infmo  9407  infsupprpr  9416  cantnfle  9590  cantnflem1  9608  epfrs  9650  frr3g  9678  updjud  9856  alephord2i  9997  cardinfima  10017  aceq3lem  10040  dfac2b  10051  dfac12lem2  10065  axdc2lem  10368  ttukeylem6  10434  alephval2  10493  fpwwe2lem11  10562  fpwwe2lem12  10563  prlem934  10954  reclem4pr  10971  suplem1pr  10973  letr  11238  sup2  12110  uzind  12619  ledivge1le  13013  xrletr  13107  xltnegi  13166  xlemul1a  13238  ixxssixx  13310  difreicc  13435  flval3  13772  fsequb  13935  seqf1olem1  14001  expnegz  14056  hash2prd  14435  ccatrcl1  14555  relexprelg  14998  shftlem  15028  rexuzre  15313  cau3lem  15315  caubnd2  15318  caubnd  15319  climrlim2  15507  climuni  15512  2clim  15532  o1co  15546  rlimno1  15614  climbdd  15632  caurcvg  15637  summolem2  15676  summo  15677  zsum  15678  fsumf1o  15683  fsumss  15685  fsumcl2lem  15691  fsumadd  15700  fsummulc2  15744  fsumconst  15750  fsumrelem  15768  prodmolem2  15898  prodmo  15899  zprod  15900  fprodf1o  15909  fprodss  15911  fprodcl2lem  15913  fprodmul  15923  fproddiv  15924  fprodconst  15941  fprodn0  15942  dfgcd2  16513  lcmfunsnlem2  16607  coprmproddvdslem  16629  cncongrprm  16697  prmpwdvds  16873  infpnlem1  16879  1arith  16896  vdwapun  16943  vdwlem11  16960  vdwnnlem2  16965  ramz  16994  ramcl  16998  prmlem0  17074  firest  17393  catpropd  17673  initoid  17966  termoid  17967  initoeu2lem1  17979  pltnle  18300  pltletr  18305  pospo  18307  psss  18544  isgrpid2  18950  f1omvdco2  19421  pgpfi  19578  frgpnabllem1  19846  gsumval3eu  19877  gsumzres  19882  gsumzcl2  19883  gsumzf1o  19885  gsumzaddlem  19894  gsumconst  19907  gsumzmhm  19910  gsumzoppg  19917  ablfaclem3  20062  dvdsrtr  20346  dvdsrmul1  20347  unitgrp  20361  domnmuln0  20688  lspsolvlem  21142  gsumfsum  21416  nzerooringczr  21462  obslbs  21712  gsummoncoe1  22301  pf1ind  22348  dmatscmcl  22493  scmatmulcl  22508  smatvscl  22514  mdetdiaglem  22588  cpmatinvcl  22707  mp2pm2mplem4  22799  cpmadugsumlemF  22866  eltg3  22952  tgidm  22970  neindisj  23107  tgrest  23149  restcld  23162  tgcn  23242  lmcnp  23294  iunconnlem  23417  2ndcredom  23440  2ndc1stc  23441  1stcrest  23443  2ndcrest  23444  2ndcdisj  23446  nllyrest  23476  nllyidm  23479  lfinpfin  23514  locfincmp  23516  ptpjpre1  23561  ptuni2  23566  ptbasin  23567  ptbasfi  23571  txbasval  23596  ptpjopn  23602  ptclsg  23605  dfac14lem  23607  xkoccn  23609  txcnp  23610  ptcnplem  23611  ptcnp  23612  txtube  23630  txcmplem1  23631  txcmplem2  23632  tx2ndc  23641  txkgen  23642  xkoco1cn  23647  xkoco2cn  23648  xkococnlem  23649  xkococn  23650  xkoinjcn  23677  qtoprest  23707  kqsat  23721  kqcldsat  23723  isfild  23848  fbunfip  23859  fgabs  23869  filconn  23873  fbasrn  23874  filufint  23910  elfm2  23938  elfm3  23940  fmfnfm  23948  hausflimi  23970  cnpflfi  23989  ptcmplem2  24043  tmdgsum2  24086  cldsubg  24101  qustgpopn  24110  ustfilxp  24203  bldisj  24388  xbln0  24404  blssps  24414  blss  24415  blssexps  24416  blssex  24417  blcls  24496  metcnp3  24530  icccmplem2  24814  mpomulcn  24859  cnheibor  24947  iscau4  25271  cmssmscld  25342  ovolshftlem2  25502  ovolicc2lem5  25513  dyadmax  25590  mbfi1fseqlem4  25710  mbfi1flimlem  25714  lhop1lem  26005  dvfsumrlim  26023  aalioulem3  26325  ulmcn  26389  radcnvlt1  26408  pilem2  26442  efopn  26647  cxpeq0  26667  cxpmul2z  26680  cxpcn3lem  26736  xrlimcnp  26957  vmappw  27104  fsumvma  27201  dchrptlem1  27252  lgsqr  27339  lgsdchrval  27342  2lgslem3  27392  2sqlem6  27411  2sqlem7  27412  2sqreultlem  27435  2sqreunnltlem  27438  pntlem3  27597  pntleml  27599  ltsval2  27645  nosupno  27692  nosupbnd1lem5  27701  noinfno  27707  lestr  27751  madebdayim  27905  ltslpss  27925  negsid  28058  noseqinds  28310  brbtwn  28993  brcgr  28994  axcontlem8  29065  nbumgrvtx  29440  cusgrfilem2  29550  1loopgrnb0  29596  uspgr2wlkeq  29739  wlklenvclwlk  29747  upgrwlkdvdelem  29829  uspgrn2crct  29901  0enwwlksnge1  29957  usgr2wspthons3  30060  clwwlkccatlem  30084  clwlkclwwlkf  30103  clwwlknonel  30190  frgrncvvdeqlem9  30402  frgr2wwlkeqm  30426  frgrreggt1  30488  frgrreg  30489  pjhthmo  31398  spansncvi  31748  nmcexi  32122  cnlnssadj  32176  leopmuli  32229  elpjrn  32286  mdsl0  32406  sumdmdii  32511  fmptcof2  32756  suppss3  32822  lmxrge0  34143  bnj594  35101  bnj849  35114  noinfepfnregs  35323  subgrwlk  35361  erdszelem7  35426  sconnpi1  35468  cvmsval  35495  cvmopnlem  35507  cvmfolem  35508  cvmliftmolem2  35511  cvmlift2lem10  35541  cvmlift2lem12  35543  cvmlift3lem5  35552  cvmlift3lem8  35555  satfv0  35587  satfv1  35592  satfvsucsuc  35594  satffunlem1lem2  35632  satffunlem2lem2  35635  linethru  36382  opnrebl2  36550  neibastop2lem  36589  neibastop2  36590  bj-cbv3ta  37140  cgsex2gd  37498  isinf2  37768  phpreu  37972  finixpnum  37973  lindsadd  37981  matunitlindflem1  37984  ptrecube  37988  poimirlem26  38014  poimirlem27  38015  poimirlem31  38019  poimir  38021  heicant  38023  voliunnfl  38032  volsupnfl  38033  itg2addnclem  38039  unirep  38082  sdclem2  38110  istotbnd3  38139  ssbnd  38156  eldisjlem19  39281  lshpdisj  39480  lsatn0  39492  lsat0cv  39526  cvrletrN  39766  cvrval4N  39907  lncvrelatN  40274  paddasslem14  40326  paddasslem15  40327  paddasslem16  40328  pmapjoin  40345  dihglblem2N  41787  dochvalr  41850  eqresfnbd  42720  sn-sup2  42982  prjspner1  43077  flt4lem7  43110  incssnn0  43161  eldioph4b  43257  diophren  43259  fphpdo  43263  rencldnfilem  43266  pellexlem5  43279  pell1234qrne0  43299  pell1234qrmulcl  43301  pell14qrgt0  43305  pell1234qrdich  43307  pell14qrdich  43315  pell1qrge1  43316  pell1qrgap  43320  pellfundre  43327  pellfundlb  43330  dvdsacongtr  43430  jm2.19lem4  43438  aomclem4  43503  hbtlem2  43570  hbtlem4  43572  hbtlem6  43575  cantnfresb  43770  dflim5  43775  tfsconcatrn  43788  tfsconcatrev  43794  naddwordnexlem4  43847  safesnsupfiss  43860  harval3  43983  clcnvlem  44068  ordpss  44895  relpfrlem  45398  cfsetsnfsetfo  47524  euoreqb  47573  2reu8i  47577  sprsymrelf1lem  47967  sprsymrelfolem2  47969  reupr  47998  fmtnofac2lem  48047  opoeALTV  48175  opeoALTV  48176  fpprwpprb  48232  gboge9  48256  clnbgrel  48320  grimco  48381  uhgrimedgi  48382  isuspgrim  48388  cycldlenngric  48420  uhgrimisgrgric  48423  clnbgrgrimlem  48425  clnbgrgrim  48426  grtriprop  48433  stgrusgra  48451  grlimedgclnbgr  48487  grlimprclnbgrvtx  48491  grlimgredgex  48492  grlictr  48507  gpgedg2iv  48559  gpgcubic  48571  gpg5nbgr3star  48573  pgnbgreunbgrlem2  48609  pgnbgreunbgrlem5  48615  ellcoellss  48927  nn0sumshdiglem1  49113  itschlc0xyqsol  49259  itsclc0  49263  opnneilv  49400