Theorem expdimp 453

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 416	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 407	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  rexlimdvv  3210  ralcom2  3373  ssexnelpss  4112  sotr3  5626  wereu2  5672  oneqmini  6413  suctr  6447  onunel  6466  fiunlem  7924  poxp  8110  suppssr  8177  suppssrg  8178  smoel  8356  omabs  8646  omsmo  8653  iiner  8779  fodomr  9124  fisseneq  9253  suplub2  9452  supnub  9453  infglb  9481  infnlb  9483  inf3lem6  9624  cfcoflem  10263  coftr  10264  zorn2lem7  10493  alephreg  10573  inar1  10766  gruen  10803  letr  11304  lbzbi  12916  xrletr  13133  xmullem  13239  supxrun  13291  ssfzoulel  13722  ssfzo12bi  13723  hashbnd  14292  fi1uzind  14454  brfi1indALT  14457  cau3lem  15297  summo  15659  mertenslem2  15827  prodmolem2  15875  alzdvds  16259  nno  16321  nn0seqcvgd  16503  lcmdvds  16541  lcmf  16566  2mulprm  16626  divgcdodd  16643  prmpwdvds  16833  catpropd  17649  pltnle  18287  pltval3  18288  pltletr  18292  tsrlemax  18535  frgpnabllem1  19735  cyggexb  19761  abvn0b  20912  isphld  21198  indistopon  22495  restntr  22677  cnprest  22784  lmss  22793  lmmo  22875  2ndcdisj  22951  txlm  23143  flftg  23491  bndth  24465  iscmet3  24801  bcthlem5  24836  ovolicc2lem4  25028  ellimc3  25387  lhop1  25522  ulmcaulem  25897  ulmcau  25898  ulmcn  25902  xrlimcnp  26462  nosepssdm  27178  ax5seglem4  28179  axcontlem2  28212  axcontlem4  28214  incistruhgr  28328  nbuhgr  28589  uhgrnbgr0nb  28600  wwlknp  29086  wwlksnred  29135  clwlkclwwlklem2a  29240  vdgn0frgrv2  29537  nmcvcn  29935  htthlem  30157  atcvat3i  31636  sumdmdlem2  31659  ifeqeqx  31761  bnj23  33717  bnj849  33924  prsrcmpltd  34074  cusgr3cyclex  34115  satffunlem2lem1  34383  funbreq  34729  cgrdegen  34964  lineext  35036  btwnconn1lem7  35053  btwnconn1lem14  35060  waj-ax  35287  lukshef-ax2  35288  relowlssretop  36232  finxpreclem6  36265  pibt2  36286  fin2solem  36462  poimirlem2  36478  poimirlem18  36494  poimirlem21  36497  poimirlem26  36502  poimirlem27  36503  poimirlem31  36507  unirep  36570  seqpo  36603  ssbnd  36644  intidl  36885  prnc  36923  eldisjlem19  37668  prtlem15  37733  lshpkrlem6  37973  atlatmstc  38177  cvrat3  38301  ps-2  38337  2lplnj  38479  paddasslem5  38683  dochkrshp4  40248  dvdsexpnn0  41227  rexlimdv3d  41406  isnacs3  41433  cantnfresb  42059  dflim5  42064  onmcl  42066  oaun3lem1  42109  pm14.24  43176  rexlim2d  44327  iccpartigtl  46077  icceuelpartlem  46089  prproropf1olem4  46160  rngcinv  46832  rngcinvALTV  46844  lindslinindsimp1  47091  lindslinindsimp2  47097  digexp  47246  aacllem  47801