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  3194  rexlimdvvva  3196  ralcom2  3340  ssexnelpss  4057  sotr3  5580  wereu2  5628  oneqmini  6377  suctr  6412  onunel  6431  fiunlem  7895  poxp  8078  suppssr  8145  suppssrg  8146  smoel  8300  omabs  8587  omsmo  8594  iiner  8736  fodomr  9066  fisseneq  9173  suplub2  9374  supnub  9375  infglb  9404  infnlb  9406  inf3lem6  9554  cfcoflem  10194  coftr  10195  zorn2lem7  10424  alephreg  10505  inar1  10698  gruen  10735  letr  11240  lbzbi  12886  xrletr  13109  xmullem  13216  supxrun  13268  ssfzoulel  13715  ssfzo12bi  13716  hashbnd  14298  fi1uzind  14469  brfi1indALT  14472  cau3lem  15317  summo  15679  mertenslem2  15850  prodmolem2  15900  alzdvds  16289  nno  16351  nn0seqcvgd  16539  lcmdvds  16577  lcmf  16602  2mulprm  16662  divgcdodd  16680  prmpwdvds  16875  catpropd  17675  pltnle  18302  pltval3  18303  pltletr  18307  tsrlemax  18552  frgpnabllem1  19848  cyggexb  19874  rngcinv  20614  abvn0b  20813  isphld  21634  indistopon  22966  restntr  23147  cnprest  23254  lmss  23263  lmmo  23345  2ndcdisj  23421  txlm  23613  flftg  23961  bndth  24925  iscmet3  25260  bcthlem5  25295  ovolicc2lem4  25487  ellimc3  25846  lhop1  25981  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  xrlimcnp  26932  nosepssdm  27650  ax5seglem4  29001  axcontlem2  29034  axcontlem4  29036  incistruhgr  29148  nbuhgr  29412  uhgrnbgr0nb  29423  wwlknp  29911  wwlksnred  29960  clwlkclwwlklem2a  30068  vdgn0frgrv2  30365  nmcvcn  30766  htthlem  30988  atcvat3i  32467  sumdmdlem2  32490  ifeqeqx  32612  bnj23  34861  bnj849  35067  prsrcmpltd  35223  cusgr3cyclex  35318  satffunlem2lem1  35586  funbreq  35952  cgrdegen  36186  lineext  36258  btwnconn1lem7  36275  btwnconn1lem14  36282  waj-ax  36596  lukshef-ax2  36597  relowlssretop  37679  finxpreclem6  37712  pibt2  37733  fin2solem  37927  poimirlem2  37943  poimirlem18  37959  poimirlem21  37962  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  unirep  38035  seqpo  38068  ssbnd  38109  intidl  38350  prnc  38388  eldisjlem19  39234  prtlem15  39321  lshpkrlem6  39561  atlatmstc  39765  cvrat3  39888  ps-2  39924  2lplnj  40066  paddasslem5  40270  dochkrshp4  41835  dvdsexpnn0  42766  rexlimdv3d  43115  isnacs3  43142  cantnfresb  43752  dflim5  43757  onmcl  43759  oaun3lem1  43802  pm14.24  44859  traxext  45404  rexlim2d  46055  iccpartigtl  47877  icceuelpartlem  47889  prproropf1olem4  47960  grimedg  48405  pgnbgreunbgrlem3  48588  pgnbgreunbgrlem6  48594  rngcinvALTV  48746  lindslinindsimp1  48927  lindslinindsimp2  48933  digexp  49077  aacllem  50270