Theorem expdimp 457

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  rexlimdvv  3220  rexlimdvvva  3222  ralcom2  3365  ssexnelpss  4070  sotr3  5609  wereu2  5657  oneqmini  6414  suctr  6449  onunel  6468  fiunlem  7937  poxp  8122  suppssr  8189  suppssrg  8190  smoel  8345  omabs  8635  omsmo  8642  iiner  8785  fodomr  9114  fisseneq  9221  suplub2  9419  supnub  9420  infglb  9449  infnlb  9451  inf3lem6  9600  cfcoflem  10262  coftr  10263  zorn2lem7  10492  alephreg  10573  inar1  10766  gruen  10803  letr  11310  lbzbi  12966  xrletr  13189  xmullem  13296  supxrun  13348  ssfzoulel  13796  ssfzo12bi  13797  hashbnd  14379  fi1uzind  14551  brfi1indALT  14554  cau3lem  15413  summo  15775  mertenslem2  15946  prodmolem2  15996  alzdvds  16384  nno  16446  nn0seqcvgd  16634  lcmdvds  16672  lcmf  16697  2mulprm  16757  divgcdodd  16775  prmpwdvds  16970  catpropd  17771  pltnle  18398  pltval3  18399  pltletr  18403  tsrlemax  18648  frgpnabllem1  19949  cyggexb  19975  rngcinv  20747  abvn0b  20950  isphld  21815  indistopon  23169  restntr  23350  cnprest  23457  lmss  23466  lmmo  23548  2ndcdisj  23624  txlm  23816  flftg  24164  bndth  25128  iscmet3  25463  bcthlem5  25498  ovolicc2lem4  25690  ellimc3  26049  lhop1  26184  ulmcaulem  26568  ulmcau  26569  ulmcn  26573  xrlimcnp  27144  nosepssdm  27861  ax5seglem4  29293  axcontlem2  29326  axcontlem4  29328  incistruhgr  29440  nbuhgr  29704  uhgrnbgr0nb  29715  wwlknp  30203  wwlksnred  30252  clwlkclwwlklem2a  30360  vdgn0frgrv2  30657  nmcvcn  31058  htthlem  31280  atcvat3i  32759  sumdmdlem2  32782  ifeqeqx  32899  bnj23  35116  bnj849  35322  prsrcmpltd  35479  cusgr3cyclex  35636  satffunlem2lem1  35904  funbreq  36270  cgrdegen  36504  lineext  36576  btwnconn1lem7  36593  btwnconn1lem14  36600  waj-ax  36953  lukshef-ax2  36954  relowlssretop  38037  finxpreclem6  38070  pibt2  38091  fin2solem  38285  poimirlem2  38301  poimirlem18  38317  poimirlem21  38320  poimirlem26  38325  poimirlem27  38326  poimirlem31  38330  unirep  38393  seqpo  38426  ssbnd  38467  intidl  38708  prnc  38746  eldisjlem19  39590  prtlem15  39677  lshpkrlem6  39917  atlatmstc  40121  cvrat3  40244  ps-2  40280  2lplnj  40422  paddasslem5  40626  dochkrshp4  42191  dvdsexpnn0  43123  rexlimdv3d  43442  isnacs3  43469  cantnfresb  44079  dflim5  44084  onmcl  44086  oaun3lem1  44129  pm14.24  45170  traxext  45714  rexlim2d  46369  iccpartigtl  48200  icceuelpartlem  48212  prproropf1olem4  48283  grimedg  48728  pgnbgreunbgrlem3  48911  pgnbgreunbgrlem6  48917  rngcinvALTV  49069  lindslinindsimp1  49265  lindslinindsimp2  49271  digexp  49415  aacllem  50649