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

This theorem is referenced by:  rexlimdvv  3205  ralcom2  3368  ssexnelpss  4109  sotr3  5623  wereu2  5669  oneqmini  6415  suctr  6449  onunel  6468  fiunlem  7939  poxp  8127  suppssr  8194  suppssrg  8195  smoel  8374  omabs  8665  omsmo  8672  iiner  8799  fodomr  9144  fisseneq  9273  suplub2  9476  supnub  9477  infglb  9505  infnlb  9507  inf3lem6  9648  cfcoflem  10287  coftr  10288  zorn2lem7  10517  alephreg  10597  inar1  10790  gruen  10827  letr  11330  lbzbi  12942  xrletr  13161  xmullem  13267  supxrun  13319  ssfzoulel  13750  ssfzo12bi  13751  hashbnd  14319  fi1uzind  14482  brfi1indALT  14485  cau3lem  15325  summo  15687  mertenslem2  15855  prodmolem2  15903  alzdvds  16288  nno  16350  nn0seqcvgd  16532  lcmdvds  16570  lcmf  16595  2mulprm  16655  divgcdodd  16672  prmpwdvds  16864  catpropd  17680  pltnle  18321  pltval3  18322  pltletr  18326  tsrlemax  18569  frgpnabllem1  19819  cyggexb  19845  rngcinv  20559  abvn0b  21240  isphld  21573  indistopon  22891  restntr  23073  cnprest  23180  lmss  23189  lmmo  23271  2ndcdisj  23347  txlm  23539  flftg  23887  bndth  24871  iscmet3  25208  bcthlem5  25243  ovolicc2lem4  25436  ellimc3  25795  lhop1  25934  ulmcaulem  26317  ulmcau  26318  ulmcn  26322  xrlimcnp  26887  nosepssdm  27606  ax5seglem4  28730  axcontlem2  28763  axcontlem4  28765  incistruhgr  28879  nbuhgr  29143  uhgrnbgr0nb  29154  wwlknp  29641  wwlksnred  29690  clwlkclwwlklem2a  29795  vdgn0frgrv2  30092  nmcvcn  30492  htthlem  30714  atcvat3i  32193  sumdmdlem2  32216  ifeqeqx  32318  bnj23  34285  bnj849  34492  prsrcmpltd  34642  cusgr3cyclex  34682  satffunlem2lem1  34950  funbreq  35301  cgrdegen  35536  lineext  35608  btwnconn1lem7  35625  btwnconn1lem14  35632  waj-ax  35834  lukshef-ax2  35835  relowlssretop  36778  finxpreclem6  36811  pibt2  36832  fin2solem  37014  poimirlem2  37030  poimirlem18  37046  poimirlem21  37049  poimirlem26  37054  poimirlem27  37055  poimirlem31  37059  unirep  37122  seqpo  37155  ssbnd  37196  intidl  37437  prnc  37475  eldisjlem19  38219  prtlem15  38284  lshpkrlem6  38524  atlatmstc  38728  cvrat3  38852  ps-2  38888  2lplnj  39030  paddasslem5  39234  dochkrshp4  40799  dvdsexpnn0  41823  rexlimdv3d  42025  isnacs3  42052  cantnfresb  42676  dflim5  42681  onmcl  42683  oaun3lem1  42726  pm14.24  43792  rexlim2d  44936  iccpartigtl  46686  icceuelpartlem  46698  prproropf1olem4  46769  rngcinvALTV  47261  lindslinindsimp1  47448  lindslinindsimp2  47454  digexp  47603  aacllem  48157