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  3193  rexlimdvvva  3195  ralcom2  3348  ssexnelpss  4069  sotr3  5574  wereu2  5622  oneqmini  6371  suctr  6406  onunel  6425  fiunlem  7889  poxp  8073  suppssr  8140  suppssrg  8141  smoel  8295  omabs  8582  omsmo  8589  iiner  8731  fodomr  9061  fisseneq  9168  suplub2  9369  supnub  9370  infglb  9399  infnlb  9401  inf3lem6  9547  cfcoflem  10187  coftr  10188  zorn2lem7  10417  alephreg  10498  inar1  10691  gruen  10728  letr  11232  lbzbi  12854  xrletr  13077  xmullem  13184  supxrun  13236  ssfzoulel  13681  ssfzo12bi  13682  hashbnd  14264  fi1uzind  14435  brfi1indALT  14438  cau3lem  15283  summo  15645  mertenslem2  15813  prodmolem2  15863  alzdvds  16252  nno  16314  nn0seqcvgd  16502  lcmdvds  16540  lcmf  16565  2mulprm  16625  divgcdodd  16642  prmpwdvds  16837  catpropd  17637  pltnle  18264  pltval3  18265  pltletr  18269  tsrlemax  18514  frgpnabllem1  19807  cyggexb  19833  rngcinv  20575  abvn0b  20774  isphld  21614  indistopon  22950  restntr  23131  cnprest  23238  lmss  23247  lmmo  23329  2ndcdisj  23405  txlm  23597  flftg  23945  bndth  24918  iscmet3  25254  bcthlem5  25289  ovolicc2lem4  25482  ellimc3  25841  lhop1  25980  ulmcaulem  26364  ulmcau  26365  ulmcn  26369  xrlimcnp  26939  nosepssdm  27659  ax5seglem4  29010  axcontlem2  29043  axcontlem4  29045  incistruhgr  29157  nbuhgr  29421  uhgrnbgr0nb  29432  wwlknp  29921  wwlksnred  29970  clwlkclwwlklem2a  30078  vdgn0frgrv2  30375  nmcvcn  30775  htthlem  30997  atcvat3i  32476  sumdmdlem2  32499  ifeqeqx  32621  bnj23  34887  bnj849  35094  prsrcmpltd  35250  cusgr3cyclex  35343  satffunlem2lem1  35611  funbreq  35977  cgrdegen  36211  lineext  36283  btwnconn1lem7  36300  btwnconn1lem14  36307  waj-ax  36621  lukshef-ax2  36622  relowlssretop  37581  finxpreclem6  37614  pibt2  37635  fin2solem  37820  poimirlem2  37836  poimirlem18  37852  poimirlem21  37855  poimirlem26  37860  poimirlem27  37861  poimirlem31  37865  unirep  37928  seqpo  37961  ssbnd  38002  intidl  38243  prnc  38281  eldisjlem19  39127  prtlem15  39214  lshpkrlem6  39454  atlatmstc  39658  cvrat3  39781  ps-2  39817  2lplnj  39959  paddasslem5  40163  dochkrshp4  41728  dvdsexpnn0  42667  rexlimdv3d  43003  isnacs3  43030  cantnfresb  43644  dflim5  43649  onmcl  43651  oaun3lem1  43694  pm14.24  44751  traxext  45296  rexlim2d  45948  iccpartigtl  47746  icceuelpartlem  47758  prproropf1olem4  47829  grimedg  48258  pgnbgreunbgrlem3  48441  pgnbgreunbgrlem6  48447  rngcinvALTV  48599  lindslinindsimp1  48780  lindslinindsimp2  48786  digexp  48930  aacllem  50123