Theorem expdimp 458

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rexlimdvv  3218  rexlimdvvva  3220  ralcom2  3362  ssexnelpss  4064  prsrcmpltd  4432  sotr3  5596  wereu2  5644  oneqmini  6405  suctr  6440  onunel  6459  fiunlem  7937  poxp  8123  suppssr  8190  suppssrg  8191  smoel  8346  omabs  8638  omsmo  8645  iiner  8788  fodomr  9125  fisseneq  9232  suplub2  9431  supnub  9432  infglb  9461  infnlb  9463  inf3lem6  9612  cfcoflem  10321  coftr  10322  zorn2lem7  10551  alephreg  10638  inar1  10831  gruen  10868  letr  11375  lbzbi  13032  xrletr  13256  xmullem  13363  supxrun  13415  ssfzoulel  13863  ssfzo12bi  13864  hashbnd  14447  fi1uzind  14619  brfi1indALT  14622  cau3lem  15489  summo  15850  mertenslem2  16021  prodmolem2  16069  alzdvds  16457  nno  16519  nn0seqcvgd  16707  lcmdvds  16745  lcmf  16770  2mulprm  16830  divgcdodd  16848  prmpwdvds  17043  catpropd  17844  pltnle  18471  pltval3  18472  pltletr  18476  tsrlemax  18721  frgpnabllem1  20048  cyggexb  20074  rngcinv  20850  abvn0b  21054  isphld  21921  indistopon  23280  restntr  23461  cnprest  23568  lmss  23577  lmmo  23659  2ndcdisj  23736  txlm  23928  flftg  24276  bndth  25240  iscmet3  25575  bcthlem5  25610  ovolicc2lem4  25802  ellimc3  26160  lhop1  26295  ulmcaulem  26684  ulmcau  26685  ulmcn  26689  xrlimcnp  27259  nosepssdm  27976  ax5seglem4  29443  axcontlem2  29476  axcontlem4  29478  incistruhgr  29590  nbuhgr  29857  uhgrnbgr0nb  29868  wwlknp  30365  wwlksnred  30414  clwlkclwwlklem2a  30522  vdgn0frgrv2  30829  nmcvcn  31230  htthlem  31452  atcvat3i  32931  sumdmdlem2  32954  ifeqeqx  33071  bnj23  35283  bnj849  35489  cusgr3cyclex  35832  satffunlem2lem1  36090  funbreq  36456  cgrdegen  36691  lineext  36763  btwnconn1lem7  36780  btwnconn1lem14  36787  waj-ax  37124  lukshef-ax2  37125  relowlssretop  38206  finxpreclem6  38239  pibt2  38260  fin2solem  38449  poimirlem2  38460  poimirlem18  38476  poimirlem21  38479  poimirlem26  38484  poimirlem27  38485  poimirlem31  38489  unirep  38568  seqpo  38601  ssbnd  38642  intidl  38883  prnc  38921  eldisjlem19  39765  prtlem15  39852  lshpkrlem6  40092  atlatmstc  40296  cvrat3  40419  ps-2  40455  2lplnj  40597  paddasslem5  40801  dochkrshp4  42366  dvdsexpnn0  43313  rexlimdv3d  43632  isnacs3  43659  cantnfresb  44269  dflim5  44274  onmcl  44276  oaun3lem1  44319  pm14.24  45360  traxext  45904  rexlim2d  46559  iccpartigtl  48427  icceuelpartlem  48439  prproropf1olem4  48510  grimedg  48955  pgnbgreunbgrlem3  49138  pgnbgreunbgrlem6  49144  rngcinvALTV  49295  lindslinindsimp1  49491  lindslinindsimp2  49497  digexp  49641  aacllem  50861