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  3191  rexlimdvvva  3193  ralcom2  3337  ssexnelpss  4049  sotr3  5569  wereu2  5617  oneqmini  6365  suctr  6400  onunel  6419  fiunlem  7884  poxp  8067  suppssr  8134  suppssrg  8135  smoel  8289  omabs  8576  omsmo  8583  iiner  8725  fodomr  9055  fisseneq  9162  suplub2  9363  supnub  9364  infglb  9393  infnlb  9395  inf3lem6  9543  cfcoflem  10183  coftr  10184  zorn2lem7  10413  alephreg  10494  inar1  10687  gruen  10724  letr  11229  lbzbi  12875  xrletr  13098  xmullem  13205  supxrun  13257  ssfzoulel  13704  ssfzo12bi  13705  hashbnd  14287  fi1uzind  14458  brfi1indALT  14461  cau3lem  15306  summo  15668  mertenslem2  15839  prodmolem2  15889  alzdvds  16278  nno  16340  nn0seqcvgd  16528  lcmdvds  16566  lcmf  16591  2mulprm  16651  divgcdodd  16669  prmpwdvds  16864  catpropd  17664  pltnle  18291  pltval3  18292  pltletr  18296  tsrlemax  18541  frgpnabllem1  19837  cyggexb  19863  rngcinv  20603  abvn0b  20802  isphld  21623  indistopon  22954  restntr  23135  cnprest  23242  lmss  23251  lmmo  23333  2ndcdisj  23409  txlm  23601  flftg  23949  bndth  24913  iscmet3  25248  bcthlem5  25283  ovolicc2lem4  25475  ellimc3  25834  lhop1  25969  ulmcaulem  26347  ulmcau  26348  ulmcn  26352  xrlimcnp  26920  nosepssdm  27638  ax5seglem4  28989  axcontlem2  29022  axcontlem4  29024  incistruhgr  29136  nbuhgr  29400  uhgrnbgr0nb  29411  wwlknp  29899  wwlksnred  29948  clwlkclwwlklem2a  30056  vdgn0frgrv2  30353  nmcvcn  30754  htthlem  30976  atcvat3i  32455  sumdmdlem2  32478  ifeqeqx  32600  bnj23  34849  bnj849  35055  prsrcmpltd  35211  cusgr3cyclex  35306  satffunlem2lem1  35574  funbreq  35940  cgrdegen  36174  lineext  36246  btwnconn1lem7  36263  btwnconn1lem14  36270  waj-ax  36584  lukshef-ax2  36585  relowlssretop  37667  finxpreclem6  37700  pibt2  37721  fin2solem  37915  poimirlem2  37931  poimirlem18  37947  poimirlem21  37950  poimirlem26  37955  poimirlem27  37956  poimirlem31  37960  unirep  38023  seqpo  38056  ssbnd  38097  intidl  38338  prnc  38376  eldisjlem19  39222  prtlem15  39309  lshpkrlem6  39549  atlatmstc  39753  cvrat3  39876  ps-2  39912  2lplnj  40054  paddasslem5  40258  dochkrshp4  41823  dvdsexpnn0  42754  rexlimdv3d  43103  isnacs3  43130  cantnfresb  43740  dflim5  43745  onmcl  43747  oaun3lem1  43790  pm14.24  44847  traxext  45392  rexlim2d  46043  iccpartigtl  47871  icceuelpartlem  47883  prproropf1olem4  47954  grimedg  48399  pgnbgreunbgrlem3  48582  pgnbgreunbgrlem6  48588  rngcinvALTV  48740  lindslinindsimp1  48921  lindslinindsimp2  48927  digexp  49071  aacllem  50264