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  3218  rexlimdvvva  3220  ralcom2  3385  ssexnelpss  4139  sotr3  5648  wereu2  5697  oneqmini  6447  suctr  6481  onunel  6500  fiunlem  7982  poxp  8169  suppssr  8236  suppssrg  8237  smoel  8416  omabs  8707  omsmo  8714  iiner  8847  fodomr  9194  fisseneq  9320  suplub2  9530  supnub  9531  infglb  9559  infnlb  9561  inf3lem6  9702  cfcoflem  10341  coftr  10342  zorn2lem7  10571  alephreg  10651  inar1  10844  gruen  10881  letr  11384  lbzbi  13001  xrletr  13220  xmullem  13326  supxrun  13378  ssfzoulel  13810  ssfzo12bi  13811  hashbnd  14385  fi1uzind  14556  brfi1indALT  14559  cau3lem  15403  summo  15765  mertenslem2  15933  prodmolem2  15983  alzdvds  16368  nno  16430  nn0seqcvgd  16617  lcmdvds  16655  lcmf  16680  2mulprm  16740  divgcdodd  16757  prmpwdvds  16951  catpropd  17767  pltnle  18408  pltval3  18409  pltletr  18413  tsrlemax  18656  frgpnabllem1  19915  cyggexb  19941  rngcinv  20659  abvn0b  20859  isphld  21695  indistopon  23029  restntr  23211  cnprest  23318  lmss  23327  lmmo  23409  2ndcdisj  23485  txlm  23677  flftg  24025  bndth  25009  iscmet3  25346  bcthlem5  25381  ovolicc2lem4  25574  ellimc3  25934  lhop1  26073  ulmcaulem  26455  ulmcau  26456  ulmcn  26460  xrlimcnp  27029  nosepssdm  27749  ax5seglem4  28965  axcontlem2  28998  axcontlem4  29000  incistruhgr  29114  nbuhgr  29378  uhgrnbgr0nb  29389  wwlknp  29876  wwlksnred  29925  clwlkclwwlklem2a  30030  vdgn0frgrv2  30327  nmcvcn  30727  htthlem  30949  atcvat3i  32428  sumdmdlem2  32451  ifeqeqx  32565  bnj23  34694  bnj849  34901  prsrcmpltd  35057  cusgr3cyclex  35104  satffunlem2lem1  35372  funbreq  35733  cgrdegen  35968  lineext  36040  btwnconn1lem7  36057  btwnconn1lem14  36064  waj-ax  36380  lukshef-ax2  36381  relowlssretop  37329  finxpreclem6  37362  pibt2  37383  fin2solem  37566  poimirlem2  37582  poimirlem18  37598  poimirlem21  37601  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  unirep  37674  seqpo  37707  ssbnd  37748  intidl  37989  prnc  38027  eldisjlem19  38766  prtlem15  38831  lshpkrlem6  39071  atlatmstc  39275  cvrat3  39399  ps-2  39435  2lplnj  39577  paddasslem5  39781  dochkrshp4  41346  dvdsexpnn0  42321  rexlimdv3d  42639  isnacs3  42666  cantnfresb  43286  dflim5  43291  onmcl  43293  oaun3lem1  43336  pm14.24  44401  traxext  44910  rexlim2d  45546  iccpartigtl  47297  icceuelpartlem  47309  prproropf1olem4  47380  grimedg  47787  rngcinvALTV  47999  lindslinindsimp1  48186  lindslinindsimp2  48192  digexp  48341  aacllem  48895