Theorem expdimp 455

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  rexlimdvv  3208  rexlimdvvva  3210  ralcom2  3354  ssexnelpss  4061  sotr3  5585  wereu2  5633  oneqmini  6384  suctr  6419  onunel  6438  fiunlem  7908  poxp  8092  suppssr  8159  suppssrg  8160  smoel  8315  omabs  8605  omsmo  8612  iiner  8755  fodomr  9085  fisseneq  9192  suplub2  9393  supnub  9394  infglb  9423  infnlb  9425  inf3lem6  9574  cfcoflem  10215  coftr  10216  zorn2lem7  10445  alephreg  10526  inar1  10719  gruen  10756  letr  11263  lbzbi  12923  xrletr  13146  xmullem  13253  supxrun  13305  ssfzoulel  13752  ssfzo12bi  13753  hashbnd  14335  fi1uzind  14506  brfi1indALT  14509  cau3lem  15354  summo  15716  mertenslem2  15887  prodmolem2  15937  alzdvds  16326  nno  16388  nn0seqcvgd  16576  lcmdvds  16614  lcmf  16639  2mulprm  16699  divgcdodd  16717  prmpwdvds  16912  catpropd  17713  pltnle  18340  pltval3  18341  pltletr  18345  tsrlemax  18590  frgpnabllem1  19885  cyggexb  19911  rngcinv  20655  abvn0b  20854  isphld  21675  indistopon  23030  restntr  23211  cnprest  23318  lmss  23327  lmmo  23409  2ndcdisj  23485  txlm  23677  flftg  24025  bndth  24989  iscmet3  25324  bcthlem5  25359  ovolicc2lem4  25551  ellimc3  25910  lhop1  26045  ulmcaulem  26423  ulmcau  26424  ulmcn  26428  xrlimcnp  26999  nosepssdm  27716  ax5seglem4  29068  axcontlem2  29101  axcontlem4  29103  incistruhgr  29215  nbuhgr  29479  uhgrnbgr0nb  29490  wwlknp  29978  wwlksnred  30027  clwlkclwwlklem2a  30135  vdgn0frgrv2  30432  nmcvcn  30833  htthlem  31055  atcvat3i  32534  sumdmdlem2  32557  ifeqeqx  32679  bnj23  34961  bnj849  35167  prsrcmpltd  35323  cusgr3cyclex  35424  satffunlem2lem1  35692  funbreq  36058  cgrdegen  36292  lineext  36364  btwnconn1lem7  36381  btwnconn1lem14  36388  waj-ax  36712  lukshef-ax2  36713  relowlssretop  37795  finxpreclem6  37828  pibt2  37849  fin2solem  38043  poimirlem2  38059  poimirlem18  38075  poimirlem21  38078  poimirlem26  38083  poimirlem27  38084  poimirlem31  38088  unirep  38151  seqpo  38184  ssbnd  38225  intidl  38466  prnc  38504  eldisjlem19  39350  prtlem15  39437  lshpkrlem6  39677  atlatmstc  39881  cvrat3  40004  ps-2  40040  2lplnj  40182  paddasslem5  40386  dochkrshp4  41951  dvdsexpnn0  42881  rexlimdv3d  43202  isnacs3  43229  cantnfresb  43839  dflim5  43844  onmcl  43846  oaun3lem1  43889  pm14.24  44946  traxext  45491  rexlim2d  46139  iccpartigtl  47967  icceuelpartlem  47979  prproropf1olem4  48050  grimedg  48495  pgnbgreunbgrlem3  48678  pgnbgreunbgrlem6  48684  rngcinvALTV  48836  lindslinindsimp1  49017  lindslinindsimp2  49023  digexp  49167  aacllem  50360