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

This theorem is referenced by:  ornld  1059  3impia  1116  ralrimdva  3107  disjiun  5062  reusv3  5329  euotd  5428  swopo  5515  wereu2  5587  poirr2  6034  sossfld  6094  reuop  6200  frpomin  6247  oneqmini  6321  suctr  6353  elpreima  6944  fmptco  7010  isofrlem  7220  onmindif2  7666  frxp  7976  fnse  7983  suppss  8019  suppssOLD  8020  tposfo2  8074  wfr3g  8147  tz7.48-2  8282  omeulem1  8422  omeu  8425  nnaordex  8478  eldifsucnn  8503  pssnn  8960  onomeneq  9020  pssnnOLD  9049  fodomfib  9102  dffi3  9199  supmo  9220  supnub  9230  infglb  9258  infnlb  9260  infmo  9263  infsupprpr  9272  cantnfle  9438  cantnflem1  9456  epfrs  9498  frr3g  9523  updjud  9701  alephord2i  9842  cardinfima  9862  aceq3lem  9885  dfac2b  9895  dfac12lem2  9909  axdc2lem  10213  ttukeylem6  10279  alephval2  10337  fpwwe2lem11  10406  fpwwe2lem12  10407  prlem934  10798  reclem4pr  10815  suplem1pr  10817  letr  11078  sup2  11940  uzind  12421  ledivge1le  12810  xrletr  12901  xltnegi  12959  xlemul1a  13031  ixxssixx  13102  difreicc  13225  flval3  13544  fsequb  13704  seqf1olem1  13771  expnegz  13826  hash2prd  14198  ccatrcl1  14308  relexprelg  14758  shftlem  14788  rexuzre  15073  cau3lem  15075  caubnd2  15078  caubnd  15079  climrlim2  15265  climuni  15270  2clim  15290  o1co  15304  rlimno1  15374  climbdd  15392  caurcvg  15397  summolem2  15437  summo  15438  zsum  15439  fsumf1o  15444  fsumss  15446  fsumcl2lem  15452  fsumadd  15461  fsummulc2  15505  fsumconst  15511  fsumrelem  15528  prodmolem2  15654  prodmo  15655  zprod  15656  fprodf1o  15665  fprodss  15667  fprodcl2lem  15669  fprodmul  15679  fproddiv  15680  fprodconst  15697  fprodn0  15698  dfgcd2  16263  lcmfunsnlem2  16354  coprmproddvdslem  16376  cncongrprm  16442  prmpwdvds  16614  infpnlem1  16620  1arith  16637  vdwapun  16684  vdwlem11  16701  vdwnnlem2  16706  ramz  16735  ramcl  16739  prmlem0  16816  firest  17152  catpropd  17427  initoid  17725  termoid  17726  initoeu2lem1  17738  pltnle  18065  pltletr  18070  pospo  18072  psss  18307  isgrpid2  18625  f1omvdco2  19065  pgpfi  19219  frgpnabllem1  19483  gsumval3eu  19514  gsumzres  19519  gsumzcl2  19520  gsumzf1o  19522  gsumzaddlem  19531  gsumconst  19544  gsumzmhm  19547  gsumzoppg  19554  ablfaclem3  19699  dvdsrtr  19903  dvdsrmul1  19904  unitgrp  19918  lspsolvlem  20413  domnmuln0  20578  gsumfsum  20674  obslbs  20946  gsummoncoe1  21484  pf1ind  21530  dmatscmcl  21661  scmatmulcl  21676  smatvscl  21682  mdetdiaglem  21756  cpmatinvcl  21875  mp2pm2mplem4  21967  cpmadugsumlemF  22034  eltg3  22121  tgidm  22139  neindisj  22277  tgrest  22319  restcld  22332  tgcn  22412  lmcnp  22464  iunconnlem  22587  2ndcredom  22610  2ndc1stc  22611  1stcrest  22613  2ndcrest  22614  2ndcdisj  22616  nllyrest  22646  nllyidm  22649  lfinpfin  22684  locfincmp  22686  ptpjpre1  22731  ptuni2  22736  ptbasin  22737  ptbasfi  22741  txbasval  22766  ptpjopn  22772  ptclsg  22775  dfac14lem  22777  xkoccn  22779  txcnp  22780  ptcnplem  22781  ptcnp  22782  txtube  22800  txcmplem1  22801  txcmplem2  22802  tx2ndc  22811  txkgen  22812  xkoco1cn  22817  xkoco2cn  22818  xkococnlem  22819  xkococn  22820  xkoinjcn  22847  qtoprest  22877  kqsat  22891  kqcldsat  22893  isfild  23018  fbunfip  23029  fgabs  23039  filconn  23043  fbasrn  23044  filufint  23080  elfm2  23108  elfm3  23110  fmfnfm  23118  hausflimi  23140  cnpflfi  23159  ptcmplem2  23213  tmdgsum2  23256  cldsubg  23271  qustgpopn  23280  ustfilxp  23373  bldisj  23560  xbln0  23576  blssps  23586  blss  23587  blssexps  23588  blssex  23589  blcls  23671  metcnp3  23705  icccmplem2  23995  cnheibor  24127  iscau4  24452  cmssmscld  24523  ovolshftlem2  24683  ovolicc2lem5  24694  dyadmax  24771  mbfi1fseqlem4  24892  mbfi1flimlem  24896  lhop1lem  25186  dvfsumrlim  25204  aalioulem3  25503  ulmcn  25567  radcnvlt1  25586  pilem2  25620  efopn  25822  cxpeq0  25842  cxpmul2z  25855  cxpcn3lem  25909  xrlimcnp  26127  vmappw  26274  fsumvma  26370  dchrptlem1  26421  lgsqr  26508  lgsdchrval  26511  2lgslem3  26561  2sqlem6  26580  2sqlem7  26581  2sqreultlem  26604  2sqreunnltlem  26607  pntlem3  26766  pntleml  26768  brbtwn  27276  brcgr  27277  axcontlem8  27348  nbumgrvtx  27722  cusgrfilem2  27832  1loopgrnb0  27878  uspgr2wlkeq  28022  wlklenvclwlk  28031  upgrwlkdvdelem  28113  uspgrn2crct  28182  0enwwlksnge1  28238  usgr2wspthons3  28338  clwwlkccatlem  28362  clwlkclwwlkf  28381  clwwlknonel  28468  frgrncvvdeqlem9  28680  frgr2wwlkeqm  28704  frgrreggt1  28766  frgrreg  28767  pjhthmo  29673  spansncvi  30023  nmcexi  30397  cnlnssadj  30451  leopmuli  30504  elpjrn  30561  mdsl0  30681  sumdmdii  30786  fmptcof2  31003  suppss3  31068  lmxrge0  31911  bnj594  32901  bnj849  32914  subgrwlk  33103  erdszelem7  33168  sconnpi1  33210  cvmsval  33237  cvmopnlem  33249  cvmfolem  33250  cvmliftmolem2  33253  cvmlift2lem10  33283  cvmlift2lem12  33285  cvmlift3lem5  33294  cvmlift3lem8  33297  satfv0  33329  satfv1  33334  satfvsucsuc  33336  satffunlem1lem2  33374  satffunlem2lem2  33377  sotr3  33742  sltval2  33868  nosupno  33915  nosupbnd1lem5  33924  noinfno  33930  sletr  33970  madebdayim  34079  sltlpss  34096  linethru  34464  opnrebl2  34519  neibastop2lem  34558  neibastop2  34559  bj-cbv3ta  34977  isinf2  35585  phpreu  35770  finixpnum  35771  lindsadd  35779  matunitlindflem1  35782  ptrecube  35786  poimirlem26  35812  poimirlem27  35813  poimirlem31  35817  poimir  35819  heicant  35821  voliunnfl  35830  volsupnfl  35831  itg2addnclem  35837  unirep  35880  sdclem2  35909  istotbnd3  35938  ssbnd  35955  lshpdisj  37008  lsatn0  37020  lsat0cv  37054  cvrletrN  37294  cvrval4N  37435  lncvrelatN  37802  paddasslem14  37854  paddasslem15  37855  paddasslem16  37856  pmapjoin  37873  dihglblem2N  39315  dochvalr  39378  sn-negex12  40405  sn-sup2  40446  prjspner1  40470  flt4lem7  40503  incssnn0  40540  eldioph4b  40640  diophren  40642  fphpdo  40646  rencldnfilem  40649  pellexlem5  40662  pell1234qrne0  40682  pell1234qrmulcl  40684  pell14qrgt0  40688  pell1234qrdich  40690  pell14qrdich  40698  pell1qrge1  40699  pell1qrgap  40703  pellfundre  40710  pellfundlb  40713  dvdsacongtr  40813  jm2.19lem4  40821  aomclem4  40889  hbtlem2  40956  hbtlem4  40958  hbtlem6  40961  harval3  41152  clcnvlem  41238  ordpss  42076  cfsetsnfsetfo  44565  euoreqb  44612  2reu8i  44616  sprsymrelf1lem  44954  sprsymrelfolem2  44956  reupr  44985  fmtnofac2lem  45031  opoeALTV  45146  opeoALTV  45147  fpprwpprb  45203  gboge9  45227  nzerooringczr  45641  ellcoellss  45787  nn0sumshdiglem1  45978  itschlc0xyqsol  46124  itsclc0  46128  opnneilv  46213