Theorem expimpd 456

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ornld  1056  3impia  1113  ralrimdva  3189  disjiun  5053  reusv3  5306  euotd  5403  swopo  5484  wereu2  5552  poirr2  5984  sossfld  6043  reuop  6144  oneqmini  6242  suctr  6274  elpreima  6828  fmptco  6891  isofrlem  7093  onmindif2  7527  frxp  7820  fnse  7827  suppss  7860  tposfo2  7915  wfr3g  7953  tz7.48-2  8078  omeulem1  8208  omeu  8211  nnaordex  8264  pssnn  8736  fodomfib  8798  dffi3  8895  supmo  8916  supnub  8926  infglb  8954  infnlb  8956  infmo  8959  infsupprpr  8968  cantnfle  9134  cantnflem1  9152  epfrs  9173  updjud  9363  alephord2i  9503  cardinfima  9523  aceq3lem  9546  dfac2b  9556  dfac12lem2  9570  axdc2lem  9870  ttukeylem6  9936  alephval2  9994  fpwwe2lem12  10063  fpwwe2lem13  10064  prlem934  10455  reclem4pr  10472  suplem1pr  10474  letr  10734  sup2  11597  uzind  12075  ledivge1le  12461  xrletr  12552  xltnegi  12610  xlemul1a  12682  ixxssixx  12753  difreicc  12871  flval3  13186  fsequb  13344  seqf1olem1  13410  expnegz  13464  hash2prd  13834  ccatrcl1  13948  relexprelg  14397  shftlem  14427  rexuzre  14712  cau3lem  14714  caubnd2  14717  caubnd  14718  climrlim2  14904  climuni  14909  2clim  14929  o1co  14943  rlimno1  15010  climbdd  15028  caurcvg  15033  summolem2  15073  summo  15074  zsum  15075  fsumf1o  15080  fsumss  15082  fsumcl2lem  15088  fsumadd  15096  fsummulc2  15139  fsumconst  15145  fsumrelem  15162  prodmolem2  15289  prodmo  15290  zprod  15291  fprodf1o  15300  fprodss  15302  fprodcl2lem  15304  fprodmul  15314  fproddiv  15315  fprodconst  15332  fprodn0  15333  dfgcd2  15894  lcmfunsnlem2  15984  coprmproddvdslem  16006  cncongrprm  16069  prmpwdvds  16240  infpnlem1  16246  1arith  16263  vdwapun  16310  vdwlem11  16327  vdwnnlem2  16332  ramz  16361  ramcl  16365  prmlem0  16439  firest  16706  catpropd  16979  initoid  17265  termoid  17266  initoeu2lem1  17274  pltnle  17576  pltletr  17581  pospo  17583  psss  17824  isgrpid2  18140  f1omvdco2  18576  pgpfi  18730  frgpnabllem1  18993  gsumval3eu  19024  gsumzres  19029  gsumzcl2  19030  gsumzf1o  19032  gsumzaddlem  19041  gsumconst  19054  gsumzmhm  19057  gsumzoppg  19064  ablfaclem3  19209  dvdsrtr  19402  dvdsrmul1  19403  unitgrp  19417  lspsolvlem  19914  domnmuln0  20071  gsummoncoe1  20472  pf1ind  20518  gsumfsum  20612  obslbs  20874  dmatscmcl  21112  scmatmulcl  21127  smatvscl  21133  mdetdiaglem  21207  cpmatinvcl  21325  mp2pm2mplem4  21417  cpmadugsumlemF  21484  eltg3  21570  tgidm  21588  neindisj  21725  tgrest  21767  restcld  21780  tgcn  21860  lmcnp  21912  iunconnlem  22035  2ndcredom  22058  2ndc1stc  22059  1stcrest  22061  2ndcrest  22062  2ndcdisj  22064  nllyrest  22094  nllyidm  22097  lfinpfin  22132  locfincmp  22134  ptpjpre1  22179  ptuni2  22184  ptbasin  22185  ptbasfi  22189  txbasval  22214  ptpjopn  22220  ptclsg  22223  dfac14lem  22225  xkoccn  22227  txcnp  22228  ptcnplem  22229  ptcnp  22230  txtube  22248  txcmplem1  22249  txcmplem2  22250  tx2ndc  22259  txkgen  22260  xkoco1cn  22265  xkoco2cn  22266  xkococnlem  22267  xkococn  22268  xkoinjcn  22295  qtoprest  22325  kqsat  22339  kqcldsat  22341  isfild  22466  fbunfip  22477  fgabs  22487  filconn  22491  fbasrn  22492  filufint  22528  elfm2  22556  elfm3  22558  fmfnfm  22566  hausflimi  22588  cnpflfi  22607  ptcmplem2  22661  tmdgsum2  22704  cldsubg  22719  qustgpopn  22728  ustfilxp  22821  bldisj  23008  xbln0  23024  blssps  23034  blss  23035  blssexps  23036  blssex  23037  blcls  23116  metcnp3  23150  icccmplem2  23431  cnheibor  23559  iscau4  23882  cmssmscld  23953  ovolshftlem2  24111  ovolicc2lem5  24122  dyadmax  24199  mbfi1fseqlem4  24319  mbfi1flimlem  24323  lhop1lem  24610  dvfsumrlim  24628  aalioulem3  24923  ulmcn  24987  radcnvlt1  25006  pilem2  25040  efopn  25241  cxpeq0  25261  cxpmul2z  25274  cxpcn3lem  25328  xrlimcnp  25546  vmappw  25693  fsumvma  25789  dchrptlem1  25840  lgsqr  25927  lgsdchrval  25930  2lgslem3  25980  2sqlem6  25999  2sqlem7  26000  2sqreultlem  26023  2sqreunnltlem  26026  pntlem3  26185  pntleml  26187  brbtwn  26685  brcgr  26686  axcontlem8  26757  nbumgrvtx  27128  cusgrfilem2  27238  1loopgrnb0  27284  uspgr2wlkeq  27427  wlklenvclwlk  27436  upgrwlkdvdelem  27517  uspgrn2crct  27586  0enwwlksnge1  27642  usgr2wspthons3  27743  clwwlkccatlem  27767  clwlkclwwlkf  27786  clwwlknonel  27874  frgrncvvdeqlem9  28086  frgr2wwlkeqm  28110  frgrreggt1  28172  frgrreg  28173  pjhthmo  29079  spansncvi  29429  nmcexi  29803  cnlnssadj  29857  leopmuli  29910  elpjrn  29967  mdsl0  30087  sumdmdii  30192  fmptcof2  30402  suppss3  30460  lmxrge0  31195  bnj594  32184  bnj849  32197  subgrwlk  32379  erdszelem7  32444  sconnpi1  32486  cvmsval  32513  cvmopnlem  32525  cvmfolem  32526  cvmliftmolem2  32529  cvmlift2lem10  32559  cvmlift2lem12  32561  cvmlift3lem5  32570  cvmlift3lem8  32573  satfv0  32605  satfv1  32610  satfvsucsuc  32612  satffunlem1lem2  32650  satffunlem2lem2  32653  sotr3  33002  trpredrec  33077  frpomin  33078  frr3g  33121  sltval2  33163  nosupno  33203  nosupbnd1lem5  33212  sletr  33237  linethru  33614  opnrebl2  33669  neibastop2lem  33708  neibastop2  33709  bj-cbv3ta  34108  isinf2  34689  phpreu  34891  finixpnum  34892  lindsadd  34900  matunitlindflem1  34903  ptrecube  34907  poimirlem26  34933  poimirlem27  34934  poimirlem31  34938  poimir  34940  heicant  34942  voliunnfl  34951  volsupnfl  34952  itg2addnclem  34958  unirep  35003  sdclem2  35032  istotbnd3  35064  ssbnd  35081  lshpdisj  36138  lsatn0  36150  lsat0cv  36184  cvrletrN  36424  cvrval4N  36565  lncvrelatN  36932  paddasslem14  36984  paddasslem15  36985  paddasslem16  36986  pmapjoin  37003  dihglblem2N  38445  dochvalr  38508  incssnn0  39328  eldioph4b  39428  diophren  39430  fphpdo  39434  rencldnfilem  39437  pellexlem5  39450  pell1234qrne0  39470  pell1234qrmulcl  39472  pell14qrgt0  39476  pell1234qrdich  39478  pell14qrdich  39486  pell1qrge1  39487  pell1qrgap  39491  pellfundre  39498  pellfundlb  39501  dvdsacongtr  39601  jm2.19lem4  39609  aomclem4  39677  hbtlem2  39744  hbtlem4  39746  hbtlem6  39749  harval3  39924  clcnvlem  40003  ordpss  40803  euoreqb  43328  2reu8i  43332  sprsymrelf1lem  43673  sprsymrelfolem2  43675  reupr  43704  fmtnofac2lem  43750  opoeALTV  43868  opeoALTV  43869  fpprwpprb  43925  gboge9  43949  nzerooringczr  44363  ellcoellss  44510  nn0sumshdiglem1  44701  itschlc0xyqsol  44774  itsclc0  44778