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  3212  rexlimdvvva  3214  ralcom2  3377  ssexnelpss  4116  sotr3  5633  wereu2  5682  oneqmini  6436  suctr  6470  onunel  6489  fiunlem  7966  poxp  8153  suppssr  8220  suppssrg  8221  smoel  8400  omabs  8689  omsmo  8696  iiner  8829  fodomr  9168  fisseneq  9293  suplub2  9501  supnub  9502  infglb  9530  infnlb  9532  inf3lem6  9673  cfcoflem  10312  coftr  10313  zorn2lem7  10542  alephreg  10622  inar1  10815  gruen  10852  letr  11355  lbzbi  12978  xrletr  13200  xmullem  13306  supxrun  13358  ssfzoulel  13799  ssfzo12bi  13800  hashbnd  14375  fi1uzind  14546  brfi1indALT  14549  cau3lem  15393  summo  15753  mertenslem2  15921  prodmolem2  15971  alzdvds  16357  nno  16419  nn0seqcvgd  16607  lcmdvds  16645  lcmf  16670  2mulprm  16730  divgcdodd  16747  prmpwdvds  16942  catpropd  17752  pltnle  18383  pltval3  18384  pltletr  18388  tsrlemax  18631  frgpnabllem1  19891  cyggexb  19917  rngcinv  20637  abvn0b  20837  isphld  21672  indistopon  23008  restntr  23190  cnprest  23297  lmss  23306  lmmo  23388  2ndcdisj  23464  txlm  23656  flftg  24004  bndth  24990  iscmet3  25327  bcthlem5  25362  ovolicc2lem4  25555  ellimc3  25914  lhop1  26053  ulmcaulem  26437  ulmcau  26438  ulmcn  26442  xrlimcnp  27011  nosepssdm  27731  ax5seglem4  28947  axcontlem2  28980  axcontlem4  28982  incistruhgr  29096  nbuhgr  29360  uhgrnbgr0nb  29371  wwlknp  29863  wwlksnred  29912  clwlkclwwlklem2a  30017  vdgn0frgrv2  30314  nmcvcn  30714  htthlem  30936  atcvat3i  32415  sumdmdlem2  32438  ifeqeqx  32555  bnj23  34732  bnj849  34939  prsrcmpltd  35095  cusgr3cyclex  35141  satffunlem2lem1  35409  funbreq  35770  cgrdegen  36005  lineext  36077  btwnconn1lem7  36094  btwnconn1lem14  36101  waj-ax  36415  lukshef-ax2  36416  relowlssretop  37364  finxpreclem6  37397  pibt2  37418  fin2solem  37613  poimirlem2  37629  poimirlem18  37645  poimirlem21  37648  poimirlem26  37653  poimirlem27  37654  poimirlem31  37658  unirep  37721  seqpo  37754  ssbnd  37795  intidl  38036  prnc  38074  eldisjlem19  38811  prtlem15  38876  lshpkrlem6  39116  atlatmstc  39320  cvrat3  39444  ps-2  39480  2lplnj  39622  paddasslem5  39826  dochkrshp4  41391  dvdsexpnn0  42369  rexlimdv3d  42694  isnacs3  42721  cantnfresb  43337  dflim5  43342  onmcl  43344  oaun3lem1  43387  pm14.24  44451  traxext  44994  rexlim2d  45640  iccpartigtl  47410  icceuelpartlem  47422  prproropf1olem4  47493  grimedg  47903  rngcinvALTV  48192  lindslinindsimp1  48374  lindslinindsimp2  48380  digexp  48528  aacllem  49320