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  3193  rexlimdvvva  3195  ralcom2  3351  ssexnelpss  4079  sotr3  5587  wereu2  5635  oneqmini  6385  suctr  6420  onunel  6439  fiunlem  7920  poxp  8107  suppssr  8174  suppssrg  8175  smoel  8329  omabs  8615  omsmo  8622  iiner  8762  fodomr  9092  fisseneq  9204  suplub2  9412  supnub  9413  infglb  9442  infnlb  9444  inf3lem6  9586  cfcoflem  10225  coftr  10226  zorn2lem7  10455  alephreg  10535  inar1  10728  gruen  10765  letr  11268  lbzbi  12895  xrletr  13118  xmullem  13224  supxrun  13276  ssfzoulel  13721  ssfzo12bi  13722  hashbnd  14301  fi1uzind  14472  brfi1indALT  14475  cau3lem  15321  summo  15683  mertenslem2  15851  prodmolem2  15901  alzdvds  16290  nno  16352  nn0seqcvgd  16540  lcmdvds  16578  lcmf  16603  2mulprm  16663  divgcdodd  16680  prmpwdvds  16875  catpropd  17670  pltnle  18297  pltval3  18298  pltletr  18302  tsrlemax  18545  frgpnabllem1  19803  cyggexb  19829  rngcinv  20546  abvn0b  20745  isphld  21563  indistopon  22888  restntr  23069  cnprest  23176  lmss  23185  lmmo  23267  2ndcdisj  23343  txlm  23535  flftg  23883  bndth  24857  iscmet3  25193  bcthlem5  25228  ovolicc2lem4  25421  ellimc3  25780  lhop1  25919  ulmcaulem  26303  ulmcau  26304  ulmcn  26308  xrlimcnp  26878  nosepssdm  27598  ax5seglem4  28859  axcontlem2  28892  axcontlem4  28894  incistruhgr  29006  nbuhgr  29270  uhgrnbgr0nb  29281  wwlknp  29773  wwlksnred  29822  clwlkclwwlklem2a  29927  vdgn0frgrv2  30224  nmcvcn  30624  htthlem  30846  atcvat3i  32325  sumdmdlem2  32348  ifeqeqx  32471  bnj23  34708  bnj849  34915  prsrcmpltd  35071  cusgr3cyclex  35123  satffunlem2lem1  35391  funbreq  35757  cgrdegen  35992  lineext  36064  btwnconn1lem7  36081  btwnconn1lem14  36088  waj-ax  36402  lukshef-ax2  36403  relowlssretop  37351  finxpreclem6  37384  pibt2  37405  fin2solem  37600  poimirlem2  37616  poimirlem18  37632  poimirlem21  37635  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  unirep  37708  seqpo  37741  ssbnd  37782  intidl  38023  prnc  38061  eldisjlem19  38802  prtlem15  38868  lshpkrlem6  39108  atlatmstc  39312  cvrat3  39436  ps-2  39472  2lplnj  39614  paddasslem5  39818  dochkrshp4  41383  dvdsexpnn0  42322  rexlimdv3d  42671  isnacs3  42698  cantnfresb  43313  dflim5  43318  onmcl  43320  oaun3lem1  43363  pm14.24  44421  traxext  44967  rexlim2d  45623  iccpartigtl  47424  icceuelpartlem  47436  prproropf1olem4  47507  grimedg  47935  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  rngcinvALTV  48264  lindslinindsimp1  48446  lindslinindsimp2  48452  digexp  48596  aacllem  49790