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  3222  rexlimdvvva  3224  ralcom2  3366  ssexnelpss  4047  prsrcmpltd  4436  sotr3  5604  wereu2  5652  oneqmini  6434  suctr  6469  onunel  6488  fiunlem  7978  poxp  8167  suppssr  8240  suppssrg  8241  smoel  8396  omabs  8688  omsmo  8695  iiner  8838  fodomr  9175  fisseneq  9282  suplub2  9480  supnub  9481  infglb  9510  infnlb  9512  inf3lem6  9661  cfcoflem  10377  coftr  10378  zorn2lem7  10607  alephreg  10694  inar1  10887  gruen  10924  letr  11431  lbzbi  13090  xrletr  13314  xmullem  13421  supxrun  13473  ssfzoulel  13922  ssfzo12bi  13923  hashbnd  14507  fi1uzind  14679  brfi1indALT  14682  cau3lem  15551  summo  15912  mertenslem2  16083  prodmolem2  16131  alzdvds  16519  nno  16581  nn0seqcvgd  16774  lcmdvds  16812  lcmf  16837  2mulprm  16897  divgcdodd  16915  prmpwdvds  17111  catpropd  17912  pltnle  18539  pltval3  18540  pltletr  18544  tsrlemax  18789  frgpnabllem1  20117  cyggexb  20143  rngcinv  20919  abvn0b  21123  isphld  21990  indistopon  23349  restntr  23530  cnprest  23637  lmss  23646  lmmo  23728  2ndcdisj  23805  txlm  23997  flftg  24345  bndth  25309  iscmet3  25644  bcthlem5  25679  ovolicc2lem4  25871  ellimc3  26229  lhop1  26364  ulmcaulem  26751  ulmcau  26752  ulmcn  26756  xrlimcnp  27326  nosepssdm  28073  ax5seglem4  29540  axcontlem2  29573  axcontlem4  29575  incistruhgr  29687  nbuhgr  29954  uhgrnbgr0nb  29965  wwlknp  30462  wwlksnred  30511  clwlkclwwlklem2a  30619  vdgn0frgrv2  30926  nmcvcn  31327  htthlem  31549  atcvat3i  33028  sumdmdlem2  33051  ifeqeqx  33210  bnj23  35419  bnj849  35625  cusgr3cyclex  36068  satffunlem2lem1  36336  funbreq  36712  cgrdegen  36947  lineext  37019  btwnconn1lem7  37036  btwnconn1lem14  37043  waj-ax  37380  lukshef-ax2  37381  relowlssretop  38478  finxpreclem6  38511  pibt2  38532  fin2solem  38721  poimirlem2  38732  poimirlem18  38748  poimirlem21  38751  poimirlem26  38756  poimirlem27  38757  poimirlem31  38761  unirep  38840  seqpo  38873  ssbnd  38914  intidl  39155  prnc  39193  eldisjlem19  40037  prtlem15  40124  lshpkrlem6  40364  atlatmstc  40568  cvrat3  40691  ps-2  40727  2lplnj  40869  paddasslem5  41073  dochkrshp4  42638  dvdsexpnn0  43579  rexlimdv3d  43886  isnacs3  43914  cantnfresb  44518  dflim5  44523  onmcl  44525  oaun3lem1  44568  pm14.24  45607  traxext  46162  rexlim2d  46842  iccpartigtl  48710  icceuelpartlem  48722  prproropf1olem4  48793  grimedg  49238  pgnbgreunbgrlem3  49421  pgnbgreunbgrlem6  49427  rngcinvALTV  49578  lindslinindsimp1  49774  lindslinindsimp2  49780  digexp  49924  aacllem  51219