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  3193  rexlimdvvva  3195  ralcom2  3348  ssexnelpss  4069  sotr3  5574  wereu2  5622  oneqmini  6371  suctr  6406  onunel  6425  fiunlem  7888  poxp  8072  suppssr  8139  suppssrg  8140  smoel  8294  omabs  8581  omsmo  8588  iiner  8730  fodomr  9060  fisseneq  9167  suplub2  9368  supnub  9369  infglb  9398  infnlb  9400  inf3lem6  9546  cfcoflem  10186  coftr  10187  zorn2lem7  10416  alephreg  10497  inar1  10690  gruen  10727  letr  11231  lbzbi  12853  xrletr  13076  xmullem  13183  supxrun  13235  ssfzoulel  13680  ssfzo12bi  13681  hashbnd  14263  fi1uzind  14434  brfi1indALT  14437  cau3lem  15282  summo  15644  mertenslem2  15812  prodmolem2  15862  alzdvds  16251  nno  16313  nn0seqcvgd  16501  lcmdvds  16539  lcmf  16564  2mulprm  16624  divgcdodd  16641  prmpwdvds  16836  catpropd  17636  pltnle  18263  pltval3  18264  pltletr  18268  tsrlemax  18513  frgpnabllem1  19806  cyggexb  19832  rngcinv  20574  abvn0b  20773  isphld  21613  indistopon  22949  restntr  23130  cnprest  23237  lmss  23246  lmmo  23328  2ndcdisj  23404  txlm  23596  flftg  23944  bndth  24917  iscmet3  25253  bcthlem5  25288  ovolicc2lem4  25481  ellimc3  25840  lhop1  25979  ulmcaulem  26363  ulmcau  26364  ulmcn  26368  xrlimcnp  26938  nosepssdm  27658  ax5seglem4  28988  axcontlem2  29021  axcontlem4  29023  incistruhgr  29135  nbuhgr  29399  uhgrnbgr0nb  29410  wwlknp  29899  wwlksnred  29948  clwlkclwwlklem2a  30056  vdgn0frgrv2  30353  nmcvcn  30753  htthlem  30975  atcvat3i  32454  sumdmdlem2  32477  ifeqeqx  32599  bnj23  34855  bnj849  35062  prsrcmpltd  35218  cusgr3cyclex  35311  satffunlem2lem1  35579  funbreq  35945  cgrdegen  36179  lineext  36251  btwnconn1lem7  36268  btwnconn1lem14  36275  waj-ax  36589  lukshef-ax2  36590  relowlssretop  37539  finxpreclem6  37572  pibt2  37593  fin2solem  37778  poimirlem2  37794  poimirlem18  37810  poimirlem21  37813  poimirlem26  37818  poimirlem27  37819  poimirlem31  37823  unirep  37886  seqpo  37919  ssbnd  37960  intidl  38201  prnc  38239  eldisjlem19  39085  prtlem15  39172  lshpkrlem6  39412  atlatmstc  39616  cvrat3  39739  ps-2  39775  2lplnj  39917  paddasslem5  40121  dochkrshp4  41686  dvdsexpnn0  42625  rexlimdv3d  42961  isnacs3  42988  cantnfresb  43602  dflim5  43607  onmcl  43609  oaun3lem1  43652  pm14.24  44709  traxext  45254  rexlim2d  45907  iccpartigtl  47705  icceuelpartlem  47717  prproropf1olem4  47788  grimedg  48217  pgnbgreunbgrlem3  48400  pgnbgreunbgrlem6  48406  rngcinvALTV  48558  lindslinindsimp1  48739  lindslinindsimp2  48745  digexp  48889  aacllem  50082