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  3185  rexlimdvvva  3187  ralcom2  3342  ssexnelpss  4069  sotr3  5572  wereu2  5620  oneqmini  6364  suctr  6399  onunel  6418  fiunlem  7884  poxp  8068  suppssr  8135  suppssrg  8136  smoel  8290  omabs  8576  omsmo  8583  iiner  8723  fodomr  9052  fisseneq  9162  suplub2  9370  supnub  9371  infglb  9400  infnlb  9402  inf3lem6  9548  cfcoflem  10185  coftr  10186  zorn2lem7  10415  alephreg  10495  inar1  10688  gruen  10725  letr  11228  lbzbi  12855  xrletr  13078  xmullem  13184  supxrun  13236  ssfzoulel  13681  ssfzo12bi  13682  hashbnd  14261  fi1uzind  14432  brfi1indALT  14435  cau3lem  15280  summo  15642  mertenslem2  15810  prodmolem2  15860  alzdvds  16249  nno  16311  nn0seqcvgd  16499  lcmdvds  16537  lcmf  16562  2mulprm  16622  divgcdodd  16639  prmpwdvds  16834  catpropd  17633  pltnle  18260  pltval3  18261  pltletr  18265  tsrlemax  18510  frgpnabllem1  19770  cyggexb  19796  rngcinv  20540  abvn0b  20739  isphld  21579  indistopon  22904  restntr  23085  cnprest  23192  lmss  23201  lmmo  23283  2ndcdisj  23359  txlm  23551  flftg  23899  bndth  24873  iscmet3  25209  bcthlem5  25244  ovolicc2lem4  25437  ellimc3  25796  lhop1  25935  ulmcaulem  26319  ulmcau  26320  ulmcn  26324  xrlimcnp  26894  nosepssdm  27614  ax5seglem4  28895  axcontlem2  28928  axcontlem4  28930  incistruhgr  29042  nbuhgr  29306  uhgrnbgr0nb  29317  wwlknp  29806  wwlksnred  29855  clwlkclwwlklem2a  29960  vdgn0frgrv2  30257  nmcvcn  30657  htthlem  30879  atcvat3i  32358  sumdmdlem2  32381  ifeqeqx  32504  bnj23  34684  bnj849  34891  prsrcmpltd  35047  cusgr3cyclex  35108  satffunlem2lem1  35376  funbreq  35742  cgrdegen  35977  lineext  36049  btwnconn1lem7  36066  btwnconn1lem14  36073  waj-ax  36387  lukshef-ax2  36388  relowlssretop  37336  finxpreclem6  37369  pibt2  37390  fin2solem  37585  poimirlem2  37601  poimirlem18  37617  poimirlem21  37620  poimirlem26  37625  poimirlem27  37626  poimirlem31  37630  unirep  37693  seqpo  37726  ssbnd  37767  intidl  38008  prnc  38046  eldisjlem19  38787  prtlem15  38853  lshpkrlem6  39093  atlatmstc  39297  cvrat3  39421  ps-2  39457  2lplnj  39599  paddasslem5  39803  dochkrshp4  41368  dvdsexpnn0  42307  rexlimdv3d  42656  isnacs3  42683  cantnfresb  43297  dflim5  43302  onmcl  43304  oaun3lem1  43347  pm14.24  44405  traxext  44951  rexlim2d  45607  iccpartigtl  47408  icceuelpartlem  47420  prproropf1olem4  47491  grimedg  47919  pgnbgreunbgrlem3  48092  pgnbgreunbgrlem6  48098  rngcinvALTV  48248  lindslinindsimp1  48430  lindslinindsimp2  48436  digexp  48580  aacllem  49774