Theorem expdimp 456

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  rexlimdvv  3219  rexlimdvvva  3221  ralcom2  3365  ssexnelpss  4071  sotr3  5597  wereu2  5645  oneqmini  6399  suctr  6434  onunel  6453  fiunlem  7923  poxp  8108  suppssr  8175  suppssrg  8176  smoel  8331  omabs  8621  omsmo  8628  iiner  8771  fodomr  9100  fisseneq  9207  suplub2  9405  supnub  9406  infglb  9435  infnlb  9437  inf3lem6  9586  cfcoflem  10240  coftr  10241  zorn2lem7  10470  alephreg  10551  inar1  10744  gruen  10781  letr  11288  lbzbi  12947  xrletr  13170  xmullem  13277  supxrun  13329  ssfzoulel  13776  ssfzo12bi  13777  hashbnd  14359  fi1uzind  14530  brfi1indALT  14533  cau3lem  15392  summo  15754  mertenslem2  15925  prodmolem2  15975  alzdvds  16364  nno  16426  nn0seqcvgd  16614  lcmdvds  16652  lcmf  16677  2mulprm  16737  divgcdodd  16755  prmpwdvds  16950  catpropd  17751  pltnle  18378  pltval3  18379  pltletr  18383  tsrlemax  18628  frgpnabllem1  19923  cyggexb  19949  rngcinv  20697  abvn0b  20892  isphld  21713  indistopon  23068  restntr  23249  cnprest  23356  lmss  23365  lmmo  23447  2ndcdisj  23523  txlm  23715  flftg  24063  bndth  25027  iscmet3  25362  bcthlem5  25397  ovolicc2lem4  25589  ellimc3  25948  lhop1  26083  ulmcaulem  26464  ulmcau  26465  ulmcn  26469  xrlimcnp  27040  nosepssdm  27757  ax5seglem4  29140  axcontlem2  29173  axcontlem4  29175  incistruhgr  29287  nbuhgr  29551  uhgrnbgr0nb  29562  wwlknp  30050  wwlksnred  30099  clwlkclwwlklem2a  30207  vdgn0frgrv2  30504  nmcvcn  30905  htthlem  31127  atcvat3i  32606  sumdmdlem2  32629  ifeqeqx  32747  bnj23  35016  bnj849  35222  prsrcmpltd  35378  cusgr3cyclex  35491  satffunlem2lem1  35759  funbreq  36125  cgrdegen  36359  lineext  36431  btwnconn1lem7  36448  btwnconn1lem14  36455  waj-ax  36779  lukshef-ax2  36780  relowlssretop  37862  finxpreclem6  37895  pibt2  37916  fin2solem  38110  poimirlem2  38126  poimirlem18  38142  poimirlem21  38145  poimirlem26  38150  poimirlem27  38151  poimirlem31  38155  unirep  38218  seqpo  38251  ssbnd  38292  intidl  38533  prnc  38571  eldisjlem19  39417  prtlem15  39504  lshpkrlem6  39744  atlatmstc  39948  cvrat3  40071  ps-2  40107  2lplnj  40249  paddasslem5  40453  dochkrshp4  42018  dvdsexpnn0  42948  rexlimdv3d  43269  isnacs3  43296  cantnfresb  43906  dflim5  43911  onmcl  43913  oaun3lem1  43956  pm14.24  44999  traxext  45544  rexlim2d  46192  iccpartigtl  48020  icceuelpartlem  48032  prproropf1olem4  48103  grimedg  48548  pgnbgreunbgrlem3  48731  pgnbgreunbgrlem6  48737  rngcinvALTV  48889  lindslinindsimp1  49070  lindslinindsimp2  49076  digexp  49220  aacllem  50413