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  3212  rexlimdvvva  3214  ralcom2  3358  ssexnelpss  4065  sotr3  5589  wereu2  5637  oneqmini  6388  suctr  6423  onunel  6442  fiunlem  7912  poxp  8096  suppssr  8163  suppssrg  8164  smoel  8319  omabs  8609  omsmo  8616  iiner  8759  fodomr  9089  fisseneq  9196  suplub2  9397  supnub  9398  infglb  9427  infnlb  9429  inf3lem6  9578  cfcoflem  10219  coftr  10220  zorn2lem7  10449  alephreg  10530  inar1  10723  gruen  10760  letr  11267  lbzbi  12927  xrletr  13150  xmullem  13257  supxrun  13309  ssfzoulel  13756  ssfzo12bi  13757  hashbnd  14339  fi1uzind  14510  brfi1indALT  14513  cau3lem  15358  summo  15720  mertenslem2  15891  prodmolem2  15941  alzdvds  16330  nno  16392  nn0seqcvgd  16580  lcmdvds  16618  lcmf  16643  2mulprm  16703  divgcdodd  16721  prmpwdvds  16916  catpropd  17717  pltnle  18344  pltval3  18345  pltletr  18349  tsrlemax  18594  frgpnabllem1  19889  cyggexb  19915  rngcinv  20659  abvn0b  20858  isphld  21679  indistopon  23034  restntr  23215  cnprest  23322  lmss  23331  lmmo  23413  2ndcdisj  23489  txlm  23681  flftg  24029  bndth  24993  iscmet3  25328  bcthlem5  25363  ovolicc2lem4  25555  ellimc3  25914  lhop1  26049  ulmcaulem  26427  ulmcau  26428  ulmcn  26432  xrlimcnp  27003  nosepssdm  27720  ax5seglem4  29072  axcontlem2  29105  axcontlem4  29107  incistruhgr  29219  nbuhgr  29483  uhgrnbgr0nb  29494  wwlknp  29982  wwlksnred  30031  clwlkclwwlklem2a  30139  vdgn0frgrv2  30436  nmcvcn  30837  htthlem  31059  atcvat3i  32538  sumdmdlem2  32561  ifeqeqx  32683  bnj23  34971  bnj849  35177  prsrcmpltd  35333  cusgr3cyclex  35434  satffunlem2lem1  35702  funbreq  36068  cgrdegen  36302  lineext  36374  btwnconn1lem7  36391  btwnconn1lem14  36398  waj-ax  36722  lukshef-ax2  36723  relowlssretop  37805  finxpreclem6  37838  pibt2  37859  fin2solem  38053  poimirlem2  38069  poimirlem18  38085  poimirlem21  38088  poimirlem26  38093  poimirlem27  38094  poimirlem31  38098  unirep  38161  seqpo  38194  ssbnd  38235  intidl  38476  prnc  38514  eldisjlem19  39360  prtlem15  39447  lshpkrlem6  39687  atlatmstc  39891  cvrat3  40014  ps-2  40050  2lplnj  40192  paddasslem5  40396  dochkrshp4  41961  dvdsexpnn0  42891  rexlimdv3d  43212  isnacs3  43239  cantnfresb  43849  dflim5  43854  onmcl  43856  oaun3lem1  43899  pm14.24  44956  traxext  45501  rexlim2d  46149  iccpartigtl  47977  icceuelpartlem  47989  prproropf1olem4  48060  grimedg  48505  pgnbgreunbgrlem3  48688  pgnbgreunbgrlem6  48694  rngcinvALTV  48846  lindslinindsimp1  49027  lindslinindsimp2  49033  digexp  49177  aacllem  50370