Theorem expdimp 458

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rexlimdvv  3220  rexlimdvvva  3222  ralcom2  3364  ssexnelpss  4068  prsrcmpltd  4436  sotr3  5608  wereu2  5656  oneqmini  6415  suctr  6450  onunel  6469  fiunlem  7942  poxp  8129  suppssr  8196  suppssrg  8197  smoel  8352  omabs  8642  omsmo  8649  iiner  8792  fodomr  9129  fisseneq  9236  suplub2  9434  supnub  9435  infglb  9464  infnlb  9466  inf3lem6  9615  cfcoflem  10277  coftr  10278  zorn2lem7  10507  alephreg  10594  inar1  10787  gruen  10824  letr  11331  lbzbi  12988  xrletr  13211  xmullem  13318  supxrun  13370  ssfzoulel  13818  ssfzo12bi  13819  hashbnd  14402  fi1uzind  14574  brfi1indALT  14577  cau3lem  15444  summo  15805  mertenslem2  15976  prodmolem2  16026  alzdvds  16414  nno  16476  nn0seqcvgd  16664  lcmdvds  16702  lcmf  16727  2mulprm  16787  divgcdodd  16805  prmpwdvds  17000  catpropd  17801  pltnle  18428  pltval3  18429  pltletr  18433  tsrlemax  18678  frgpnabllem1  20001  cyggexb  20027  rngcinv  20800  abvn0b  21003  isphld  21868  indistopon  23227  restntr  23408  cnprest  23515  lmss  23524  lmmo  23606  2ndcdisj  23683  txlm  23875  flftg  24223  bndth  25187  iscmet3  25522  bcthlem5  25557  ovolicc2lem4  25749  ellimc3  26108  lhop1  26243  ulmcaulem  26627  ulmcau  26628  ulmcn  26632  xrlimcnp  27203  nosepssdm  27920  ax5seglem4  29375  axcontlem2  29408  axcontlem4  29410  incistruhgr  29522  nbuhgr  29789  uhgrnbgr0nb  29800  wwlknp  30297  wwlksnred  30346  clwlkclwwlklem2a  30454  vdgn0frgrv2  30761  nmcvcn  31162  htthlem  31384  atcvat3i  32863  sumdmdlem2  32886  ifeqeqx  33003  bnj23  35215  bnj849  35421  cusgr3cyclex  35712  satffunlem2lem1  35970  funbreq  36336  cgrdegen  36571  lineext  36643  btwnconn1lem7  36660  btwnconn1lem14  36667  waj-ax  37020  lukshef-ax2  37021  relowlssretop  38104  finxpreclem6  38137  pibt2  38158  fin2solem  38347  poimirlem2  38358  poimirlem18  38374  poimirlem21  38377  poimirlem26  38382  poimirlem27  38383  poimirlem31  38387  unirep  38451  seqpo  38484  ssbnd  38525  intidl  38766  prnc  38804  eldisjlem19  39648  prtlem15  39735  lshpkrlem6  39975  atlatmstc  40179  cvrat3  40302  ps-2  40338  2lplnj  40480  paddasslem5  40684  dochkrshp4  42249  dvdsexpnn0  43196  rexlimdv3d  43515  isnacs3  43542  cantnfresb  44152  dflim5  44157  onmcl  44159  oaun3lem1  44202  pm14.24  45243  traxext  45787  rexlim2d  46442  iccpartigtl  48310  icceuelpartlem  48322  prproropf1olem4  48393  grimedg  48838  pgnbgreunbgrlem3  49021  pgnbgreunbgrlem6  49027  rngcinvALTV  49178  lindslinindsimp1  49374  lindslinindsimp2  49380  digexp  49524  aacllem  50759