Theorem expimpd 627

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ornld  938  ralrimdva  2952  disjiun  4573  reusv3  4802  ralxfrdOLD  4806  euotd  4900  swopo  4969  wereu2  5035  poirr2  5439  sossfld  5499  oneqmini  5693  suctr  5725  elpreima  6245  fmptco  6303  isofrlem  6490  onmindif2  6904  frxp  7174  fnse  7181  suppss  7212  tposfo2  7262  wfr3g  7300  tz7.48-2  7424  omeulem1  7549  omeu  7552  nnaordex  7605  pssnn  8063  fodomfib  8125  dffi3  8220  supmo  8241  supnub  8251  infglb  8279  infnlb  8281  infmo  8284  cantnfle  8451  cantnflem1  8469  epfrs  8490  alephord2i  8783  cardinfima  8803  aceq3lem  8826  dfac2  8836  dfac12lem2  8849  axdc2lem  9153  ttukeylem6  9219  alephval2  9273  fpwwe2lem12  9342  fpwwe2lem13  9343  prlem934  9734  reclem4pr  9751  suplem1pr  9753  letr  10010  sup2  10858  uzind  11345  ledivge1le  11777  xrletr  11865  xltnegi  11921  xlemul1a  11990  ixxssixx  12060  difreicc  12175  flval3  12478  fsequb  12636  seqf1olem1  12702  expnegz  12756  hash2prd  13114  ccatrcl1  13229  relexprelg  13626  shftlem  13656  rexuzre  13940  cau3lem  13942  caubnd2  13945  caubnd  13946  climrlim2  14126  climuni  14131  2clim  14151  o1co  14165  rlimno1  14232  climbdd  14250  caurcvg  14255  summolem2  14294  summo  14295  zsum  14296  fsumf1o  14301  fsumss  14303  fsumcl2lem  14309  fsumadd  14317  fsummulc2  14358  fsumconst  14364  fsumrelem  14380  prodmolem2  14504  prodmo  14505  zprod  14506  fprodf1o  14515  fprodss  14517  fprodcl2lem  14519  fprodmul  14529  fproddiv  14530  fprodconst  14547  fprodn0  14548  dfgcd2  15101  coprmproddvdslem  15214  cncongrprm  15275  prmpwdvds  15446  infpnlem1  15452  1arith  15469  vdwapun  15516  vdwlem11  15533  vdwnnlem2  15538  ramz  15567  ramcl  15571  prmlem0  15650  firest  15916  catpropd  16192  initoid  16478  termoid  16479  initoeu2lem1  16487  pltnle  16789  pltletr  16794  pospo  16796  psss  17037  isgrpid2  17281  f1omvdco2  17691  pgpfi  17843  frgpnabllem1  18099  gsumval3eu  18128  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  gsumzoppg  18167  ablfaclem3  18309  dvdsrtr  18475  dvdsrmul1  18476  unitgrp  18490  lspsolvlem  18963  domnmuln0  19119  gsummoncoe1  19495  pf1ind  19540  gsumfsum  19632  obslbs  19893  dmatscmcl  20128  scmatmulcl  20143  smatvscl  20149  mdetdiaglem  20223  cpmatinvcl  20341  mp2pm2mplem4  20433  cpmadugsumlemF  20500  eltg3  20577  tgidm  20595  neindisj  20731  tgrest  20773  restcld  20786  tgcn  20866  lmcnp  20918  iunconlem  21040  2ndcredom  21063  2ndc1stc  21064  1stcrest  21066  2ndcrest  21067  2ndcdisj  21069  nllyrest  21099  nllyidm  21102  lfinpfin  21137  locfincmp  21139  ptpjpre1  21184  ptuni2  21189  ptbasin  21190  ptbasfi  21194  txbasval  21219  ptpjopn  21225  ptclsg  21228  dfac14lem  21230  xkoccn  21232  txcnp  21233  ptcnplem  21234  ptcnp  21235  txtube  21253  txcmplem1  21254  txcmplem2  21255  tx2ndc  21264  txkgen  21265  xkoco1cn  21270  xkoco2cn  21271  xkococnlem  21272  xkococn  21273  xkoinjcn  21300  qtoprest  21330  kqsat  21344  kqcldsat  21346  isfild  21472  fbunfip  21483  fgabs  21493  filcon  21497  fbasrn  21498  filufint  21534  elfm2  21562  elfm3  21564  fmfnfm  21572  hausflimi  21594  cnpflfi  21613  ptcmplem2  21667  tmdgsum2  21710  cldsubg  21724  qustgpopn  21733  ustfilxp  21826  bldisj  22013  xbln0  22029  blssps  22039  blss  22040  blssexps  22041  blssex  22042  blcls  22121  metcnp3  22155  icccmplem2  22434  cnheibor  22562  iscau4  22885  ovolshftlem2  23085  ovolicc2lem5  23096  dyadmax  23172  mbfi1fseqlem4  23291  mbfi1flimlem  23295  lhop1lem  23580  dvfsumrlim  23598  aalioulem3  23893  ulmcn  23957  radcnvlt1  23976  pilem2  24010  efopn  24204  cxpeq0  24224  cxpmul2z  24237  cxpcn3lem  24288  xrlimcnp  24495  vmappw  24642  fsumvma  24738  dchrptlem1  24789  lgsqr  24876  lgsdchrval  24879  2lgslem3  24929  2sqlem6  24948  2sqlem7  24949  pntlem3  25098  pntleml  25100  brbtwn  25579  brcgr  25580  axcontlem8  25651  cusgrafilem2  26008  redwlk  26136  4cycl4dv  26195  cusconngra  26204  usg2wlkeq  26236  usg2spthonot  26415  usg2spthonot0  26416  frg2woteq  26587  pjhthmo  27545  spansncvi  27895  nmcexi  28269  cnlnssadj  28323  leopmuli  28376  elpjrn  28433  mdsl0  28553  sumdmdii  28658  fmptcof2  28839  suppss3  28890  lmxrge0  29326  bnj594  30236  bnj849  30249  erdszelem7  30433  sconpi1  30475  cvmsval  30502  cvmopnlem  30514  cvmfolem  30515  cvmliftmolem2  30518  cvmlift2lem10  30548  cvmlift2lem12  30550  cvmlift3lem5  30559  cvmlift3lem8  30562  trpredrec  30982  frr3g  31023  sltval2  31053  linethru  31430  opnrebl2  31486  neibastop2lem  31525  neibastop2  31526  bj-ssbequ1  31833  bj-cbv3ta  31897  phpreu  32563  finixpnum  32564  matunitlindflem1  32575  ptrecube  32579  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  poimir  32612  heicant  32614  voliunnfl  32623  volsupnfl  32624  itg2addnclem  32631  unirep  32677  sdclem2  32708  istotbnd3  32740  ssbnd  32757  lshpdisj  33292  lsatn0  33304  lsat0cv  33338  cvrletrN  33578  cvrval4N  33718  lncvrelatN  34085  paddasslem14  34137  paddasslem15  34138  paddasslem16  34139  pmapjoin  34156  dihglblem2N  35601  dochvalr  35664  incssnn0  36292  eldioph4b  36393  diophren  36395  fphpdo  36399  rencldnfilem  36402  pellexlem5  36415  pell1234qrne0  36435  pell1234qrmulcl  36437  pell14qrgt0  36441  pell1234qrdich  36443  pell14qrdich  36451  pell1qrge1  36452  pell1qrgap  36456  pellfundre  36463  pellfundlb  36466  dvdsacongtr  36569  jm2.19lem4  36577  aomclem4  36645  hbtlem2  36713  hbtlem4  36715  hbtlem6  36718  clcnvlem  36949  ordpss  37676  fmtnofac2lem  40018  opoeALTV  40132  opeoALTV  40133  gboage9  40186  nbumgrvtx  40568  cusgrfilem2  40672  1loopgrnb0  40717  uspgr2wlkeq  40854  upgrwlkdvdelem  40942  uspgrn2crct  41011  0enwwlksnge1  41060  usgr2wspthons3  41167  frgr2wwlkeqm  41496  av-frgrareggt1  41547  av-frgrareg  41548  nzerooringczr  41864  ellcoellss  42018  nn0sumshdiglem1  42213