Theorem expdimp 454

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 417	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 408	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  rexlimdvv  3211  ralcom2  3374  ssexnelpss  4114  sotr3  5628  wereu2  5674  oneqmini  6417  suctr  6451  onunel  6470  fiunlem  7928  poxp  8114  suppssr  8181  suppssrg  8182  smoel  8360  omabs  8650  omsmo  8657  iiner  8783  fodomr  9128  fisseneq  9257  suplub2  9456  supnub  9457  infglb  9485  infnlb  9487  inf3lem6  9628  cfcoflem  10267  coftr  10268  zorn2lem7  10497  alephreg  10577  inar1  10770  gruen  10807  letr  11308  lbzbi  12920  xrletr  13137  xmullem  13243  supxrun  13295  ssfzoulel  13726  ssfzo12bi  13727  hashbnd  14296  fi1uzind  14458  brfi1indALT  14461  cau3lem  15301  summo  15663  mertenslem2  15831  prodmolem2  15879  alzdvds  16263  nno  16325  nn0seqcvgd  16507  lcmdvds  16545  lcmf  16570  2mulprm  16630  divgcdodd  16647  prmpwdvds  16837  catpropd  17653  pltnle  18291  pltval3  18292  pltletr  18296  tsrlemax  18539  frgpnabllem1  19741  cyggexb  19767  abvn0b  20920  isphld  21207  indistopon  22504  restntr  22686  cnprest  22793  lmss  22802  lmmo  22884  2ndcdisj  22960  txlm  23152  flftg  23500  bndth  24474  iscmet3  24810  bcthlem5  24845  ovolicc2lem4  25037  ellimc3  25396  lhop1  25531  ulmcaulem  25906  ulmcau  25907  ulmcn  25911  xrlimcnp  26473  nosepssdm  27189  ax5seglem4  28190  axcontlem2  28223  axcontlem4  28225  incistruhgr  28339  nbuhgr  28600  uhgrnbgr0nb  28611  wwlknp  29097  wwlksnred  29146  clwlkclwwlklem2a  29251  vdgn0frgrv2  29548  nmcvcn  29948  htthlem  30170  atcvat3i  31649  sumdmdlem2  31672  ifeqeqx  31774  bnj23  33729  bnj849  33936  prsrcmpltd  34086  cusgr3cyclex  34127  satffunlem2lem1  34395  funbreq  34741  cgrdegen  34976  lineext  35048  btwnconn1lem7  35065  btwnconn1lem14  35072  waj-ax  35299  lukshef-ax2  35300  relowlssretop  36244  finxpreclem6  36277  pibt2  36298  fin2solem  36474  poimirlem2  36490  poimirlem18  36506  poimirlem21  36509  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  unirep  36582  seqpo  36615  ssbnd  36656  intidl  36897  prnc  36935  eldisjlem19  37680  prtlem15  37745  lshpkrlem6  37985  atlatmstc  38189  cvrat3  38313  ps-2  38349  2lplnj  38491  paddasslem5  38695  dochkrshp4  40260  dvdsexpnn0  41232  rexlimdv3d  41421  isnacs3  41448  cantnfresb  42074  dflim5  42079  onmcl  42081  oaun3lem1  42124  pm14.24  43191  rexlim2d  44341  iccpartigtl  46091  icceuelpartlem  46103  prproropf1olem4  46174  rngcinv  46879  rngcinvALTV  46891  lindslinindsimp1  47138  lindslinindsimp2  47144  digexp  47293  aacllem  47848