Theorem expdimp 452

Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)

Hypothesis

Ref	Expression
expdimp.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expdimp	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem expdimp

Step	Hyp	Ref	Expression
1		expdimp.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 415	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 406	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  rexlimdvv  3209  rexlimdvvva  3211  ralcom2  3374  ssexnelpss  4125  sotr3  5636  wereu2  5685  oneqmini  6437  suctr  6471  onunel  6490  fiunlem  7964  poxp  8151  suppssr  8218  suppssrg  8219  smoel  8398  omabs  8687  omsmo  8694  iiner  8827  fodomr  9166  fisseneq  9290  suplub2  9498  supnub  9499  infglb  9527  infnlb  9529  inf3lem6  9670  cfcoflem  10309  coftr  10310  zorn2lem7  10539  alephreg  10619  inar1  10812  gruen  10849  letr  11352  lbzbi  12975  xrletr  13196  xmullem  13302  supxrun  13354  ssfzoulel  13795  ssfzo12bi  13796  hashbnd  14371  fi1uzind  14542  brfi1indALT  14545  cau3lem  15389  summo  15749  mertenslem2  15917  prodmolem2  15967  alzdvds  16353  nno  16415  nn0seqcvgd  16603  lcmdvds  16641  lcmf  16666  2mulprm  16726  divgcdodd  16743  prmpwdvds  16937  catpropd  17753  pltnle  18395  pltval3  18396  pltletr  18400  tsrlemax  18643  frgpnabllem1  19905  cyggexb  19931  rngcinv  20653  abvn0b  20853  isphld  21689  indistopon  23023  restntr  23205  cnprest  23312  lmss  23321  lmmo  23403  2ndcdisj  23479  txlm  23671  flftg  24019  bndth  25003  iscmet3  25340  bcthlem5  25375  ovolicc2lem4  25568  ellimc3  25928  lhop1  26067  ulmcaulem  26451  ulmcau  26452  ulmcn  26456  xrlimcnp  27025  nosepssdm  27745  ax5seglem4  28961  axcontlem2  28994  axcontlem4  28996  incistruhgr  29110  nbuhgr  29374  uhgrnbgr0nb  29385  wwlknp  29872  wwlksnred  29921  clwlkclwwlklem2a  30026  vdgn0frgrv2  30323  nmcvcn  30723  htthlem  30945  atcvat3i  32424  sumdmdlem2  32447  ifeqeqx  32562  bnj23  34710  bnj849  34917  prsrcmpltd  35073  cusgr3cyclex  35120  satffunlem2lem1  35388  funbreq  35750  cgrdegen  35985  lineext  36057  btwnconn1lem7  36074  btwnconn1lem14  36081  waj-ax  36396  lukshef-ax2  36397  relowlssretop  37345  finxpreclem6  37378  pibt2  37399  fin2solem  37592  poimirlem2  37608  poimirlem18  37624  poimirlem21  37627  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  unirep  37700  seqpo  37733  ssbnd  37774  intidl  38015  prnc  38053  eldisjlem19  38791  prtlem15  38856  lshpkrlem6  39096  atlatmstc  39300  cvrat3  39424  ps-2  39460  2lplnj  39602  paddasslem5  39806  dochkrshp4  41371  dvdsexpnn0  42347  rexlimdv3d  42670  isnacs3  42697  cantnfresb  43313  dflim5  43318  onmcl  43320  oaun3lem1  43363  pm14.24  44427  traxext  44937  rexlim2d  45580  iccpartigtl  47347  icceuelpartlem  47359  prproropf1olem4  47430  grimedg  47840  rngcinvALTV  48119  lindslinindsimp1  48302  lindslinindsimp2  48308  digexp  48456  aacllem  49031