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  3197  rexlimdvvva  3199  ralcom2  3356  ssexnelpss  4091  sotr3  5602  wereu2  5651  oneqmini  6405  suctr  6440  onunel  6459  fiunlem  7940  poxp  8127  suppssr  8194  suppssrg  8195  smoel  8374  omabs  8663  omsmo  8670  iiner  8803  fodomr  9142  fisseneq  9265  suplub2  9473  supnub  9474  infglb  9503  infnlb  9505  inf3lem6  9647  cfcoflem  10286  coftr  10287  zorn2lem7  10516  alephreg  10596  inar1  10789  gruen  10826  letr  11329  lbzbi  12952  xrletr  13174  xmullem  13280  supxrun  13332  ssfzoulel  13776  ssfzo12bi  13777  hashbnd  14354  fi1uzind  14525  brfi1indALT  14528  cau3lem  15373  summo  15733  mertenslem2  15901  prodmolem2  15951  alzdvds  16339  nno  16401  nn0seqcvgd  16589  lcmdvds  16627  lcmf  16652  2mulprm  16712  divgcdodd  16729  prmpwdvds  16924  catpropd  17721  pltnle  18348  pltval3  18349  pltletr  18353  tsrlemax  18596  frgpnabllem1  19854  cyggexb  19880  rngcinv  20597  abvn0b  20796  isphld  21614  indistopon  22939  restntr  23120  cnprest  23227  lmss  23236  lmmo  23318  2ndcdisj  23394  txlm  23586  flftg  23934  bndth  24908  iscmet3  25245  bcthlem5  25280  ovolicc2lem4  25473  ellimc3  25832  lhop1  25971  ulmcaulem  26355  ulmcau  26356  ulmcn  26360  xrlimcnp  26930  nosepssdm  27650  ax5seglem4  28911  axcontlem2  28944  axcontlem4  28946  incistruhgr  29058  nbuhgr  29322  uhgrnbgr0nb  29333  wwlknp  29825  wwlksnred  29874  clwlkclwwlklem2a  29979  vdgn0frgrv2  30276  nmcvcn  30676  htthlem  30898  atcvat3i  32377  sumdmdlem2  32400  ifeqeqx  32523  bnj23  34749  bnj849  34956  prsrcmpltd  35112  cusgr3cyclex  35158  satffunlem2lem1  35426  funbreq  35787  cgrdegen  36022  lineext  36094  btwnconn1lem7  36111  btwnconn1lem14  36118  waj-ax  36432  lukshef-ax2  36433  relowlssretop  37381  finxpreclem6  37414  pibt2  37435  fin2solem  37630  poimirlem2  37646  poimirlem18  37662  poimirlem21  37665  poimirlem26  37670  poimirlem27  37671  poimirlem31  37675  unirep  37738  seqpo  37771  ssbnd  37812  intidl  38053  prnc  38091  eldisjlem19  38828  prtlem15  38893  lshpkrlem6  39133  atlatmstc  39337  cvrat3  39461  ps-2  39497  2lplnj  39639  paddasslem5  39843  dochkrshp4  41408  dvdsexpnn0  42383  rexlimdv3d  42706  isnacs3  42733  cantnfresb  43348  dflim5  43353  onmcl  43355  oaun3lem1  43398  pm14.24  44456  traxext  45002  rexlim2d  45654  iccpartigtl  47437  icceuelpartlem  47449  prproropf1olem4  47520  grimedg  47948  rngcinvALTV  48251  lindslinindsimp1  48433  lindslinindsimp2  48439  digexp  48587  aacllem  49665