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  3186  rexlimdvvva  3188  ralcom2  3341  ssexnelpss  4064  sotr3  5563  wereu2  5611  oneqmini  6355  suctr  6390  onunel  6409  fiunlem  7869  poxp  8053  suppssr  8120  suppssrg  8121  smoel  8275  omabs  8561  omsmo  8568  iiner  8708  fodomr  9036  fisseneq  9142  suplub2  9340  supnub  9341  infglb  9370  infnlb  9372  inf3lem6  9518  cfcoflem  10155  coftr  10156  zorn2lem7  10385  alephreg  10465  inar1  10658  gruen  10695  letr  11199  lbzbi  12826  xrletr  13049  xmullem  13155  supxrun  13207  ssfzoulel  13652  ssfzo12bi  13653  hashbnd  14235  fi1uzind  14406  brfi1indALT  14409  cau3lem  15254  summo  15616  mertenslem2  15784  prodmolem2  15834  alzdvds  16223  nno  16285  nn0seqcvgd  16473  lcmdvds  16511  lcmf  16536  2mulprm  16596  divgcdodd  16613  prmpwdvds  16808  catpropd  17607  pltnle  18234  pltval3  18235  pltletr  18239  tsrlemax  18484  frgpnabllem1  19778  cyggexb  19804  rngcinv  20545  abvn0b  20744  isphld  21584  indistopon  22909  restntr  23090  cnprest  23197  lmss  23206  lmmo  23288  2ndcdisj  23364  txlm  23556  flftg  23904  bndth  24877  iscmet3  25213  bcthlem5  25248  ovolicc2lem4  25441  ellimc3  25800  lhop1  25939  ulmcaulem  26323  ulmcau  26324  ulmcn  26328  xrlimcnp  26898  nosepssdm  27618  ax5seglem4  28903  axcontlem2  28936  axcontlem4  28938  incistruhgr  29050  nbuhgr  29314  uhgrnbgr0nb  29325  wwlknp  29814  wwlksnred  29863  clwlkclwwlklem2a  29968  vdgn0frgrv2  30265  nmcvcn  30665  htthlem  30887  atcvat3i  32366  sumdmdlem2  32389  ifeqeqx  32512  bnj23  34720  bnj849  34927  prsrcmpltd  35083  cusgr3cyclex  35148  satffunlem2lem1  35416  funbreq  35782  cgrdegen  36017  lineext  36089  btwnconn1lem7  36106  btwnconn1lem14  36113  waj-ax  36427  lukshef-ax2  36428  relowlssretop  37376  finxpreclem6  37409  pibt2  37430  fin2solem  37625  poimirlem2  37641  poimirlem18  37657  poimirlem21  37660  poimirlem26  37665  poimirlem27  37666  poimirlem31  37670  unirep  37733  seqpo  37766  ssbnd  37807  intidl  38048  prnc  38086  eldisjlem19  38827  prtlem15  38893  lshpkrlem6  39133  atlatmstc  39337  cvrat3  39460  ps-2  39496  2lplnj  39638  paddasslem5  39842  dochkrshp4  41407  dvdsexpnn0  42346  rexlimdv3d  42695  isnacs3  42722  cantnfresb  43336  dflim5  43341  onmcl  43343  oaun3lem1  43386  pm14.24  44444  traxext  44989  rexlim2d  45644  iccpartigtl  47433  icceuelpartlem  47445  prproropf1olem4  47516  grimedg  47945  pgnbgreunbgrlem3  48128  pgnbgreunbgrlem6  48134  rngcinvALTV  48286  lindslinindsimp1  48468  lindslinindsimp2  48474  digexp  48618  aacllem  49812