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  3194  rexlimdvvva  3196  ralcom2  3340  ssexnelpss  4057  sotr3  5571  wereu2  5619  oneqmini  6368  suctr  6403  onunel  6422  fiunlem  7886  poxp  8069  suppssr  8136  suppssrg  8137  smoel  8291  omabs  8578  omsmo  8585  iiner  8727  fodomr  9057  fisseneq  9164  suplub2  9365  supnub  9366  infglb  9395  infnlb  9397  inf3lem6  9543  cfcoflem  10183  coftr  10184  zorn2lem7  10413  alephreg  10494  inar1  10687  gruen  10724  letr  11228  lbzbi  12850  xrletr  13073  xmullem  13180  supxrun  13232  ssfzoulel  13677  ssfzo12bi  13678  hashbnd  14260  fi1uzind  14431  brfi1indALT  14434  cau3lem  15279  summo  15641  mertenslem2  15809  prodmolem2  15859  alzdvds  16248  nno  16310  nn0seqcvgd  16498  lcmdvds  16536  lcmf  16561  2mulprm  16621  divgcdodd  16638  prmpwdvds  16833  catpropd  17633  pltnle  18260  pltval3  18261  pltletr  18265  tsrlemax  18510  frgpnabllem1  19806  cyggexb  19832  rngcinv  20572  abvn0b  20771  isphld  21611  indistopon  22944  restntr  23125  cnprest  23232  lmss  23241  lmmo  23323  2ndcdisj  23399  txlm  23591  flftg  23939  bndth  24903  iscmet3  25238  bcthlem5  25273  ovolicc2lem4  25465  ellimc3  25824  lhop1  25960  ulmcaulem  26343  ulmcau  26344  ulmcn  26348  xrlimcnp  26918  nosepssdm  27638  ax5seglem4  28989  axcontlem2  29022  axcontlem4  29024  incistruhgr  29136  nbuhgr  29400  uhgrnbgr0nb  29411  wwlknp  29900  wwlksnred  29949  clwlkclwwlklem2a  30057  vdgn0frgrv2  30354  nmcvcn  30755  htthlem  30977  atcvat3i  32456  sumdmdlem2  32479  ifeqeqx  32601  bnj23  34867  bnj849  35073  prsrcmpltd  35229  cusgr3cyclex  35324  satffunlem2lem1  35592  funbreq  35958  cgrdegen  36192  lineext  36264  btwnconn1lem7  36281  btwnconn1lem14  36288  waj-ax  36602  lukshef-ax2  36603  relowlssretop  37675  finxpreclem6  37708  pibt2  37729  fin2solem  37918  poimirlem2  37934  poimirlem18  37950  poimirlem21  37953  poimirlem26  37958  poimirlem27  37959  poimirlem31  37963  unirep  38026  seqpo  38059  ssbnd  38100  intidl  38341  prnc  38379  eldisjlem19  39225  prtlem15  39312  lshpkrlem6  39552  atlatmstc  39756  cvrat3  39879  ps-2  39915  2lplnj  40057  paddasslem5  40261  dochkrshp4  41826  dvdsexpnn0  42765  rexlimdv3d  43114  isnacs3  43141  cantnfresb  43755  dflim5  43760  onmcl  43762  oaun3lem1  43805  pm14.24  44862  traxext  45407  rexlim2d  46059  iccpartigtl  47857  icceuelpartlem  47869  prproropf1olem4  47940  grimedg  48369  pgnbgreunbgrlem3  48552  pgnbgreunbgrlem6  48558  rngcinvALTV  48710  lindslinindsimp1  48891  lindslinindsimp2  48897  digexp  49041  aacllem  50234