Theorem expdimp 455

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  rexlimdvv  3293  ralcom2  3363  ssexnelpss  4090  wereu2  5552  oneqmini  6242  suctr  6274  fiunlem  7643  poxp  7822  suppssr  7861  smoel  7997  omabs  8274  omsmo  8281  iiner  8369  fodomr  8668  fisseneq  8729  suplub2  8925  supnub  8926  infglb  8954  infnlb  8956  inf3lem6  9096  cfcoflem  9694  coftr  9695  zorn2lem7  9924  alephreg  10004  inar1  10197  gruen  10234  letr  10734  lbzbi  12337  xrletr  12552  xmullem  12658  supxrun  12710  ssfzoulel  13132  ssfzo12bi  13133  hashbnd  13697  fi1uzind  13856  brfi1indALT  13859  cau3lem  14714  summo  15074  mertenslem2  15241  prodmolem2  15289  alzdvds  15670  nno  15733  nn0seqcvgd  15914  lcmdvds  15952  lcmf  15977  2mulprm  16037  divgcdodd  16054  prmpwdvds  16240  catpropd  16979  pltnle  17576  pltval3  17577  pltletr  17581  tsrlemax  17830  frgpnabllem1  18993  cyggexb  19019  abvn0b  20075  isphld  20798  indistopon  21609  restntr  21790  cnprest  21897  lmss  21906  lmmo  21988  2ndcdisj  22064  txlm  22256  flftg  22604  bndth  23562  iscmet3  23896  bcthlem5  23931  ovolicc2lem4  24121  ellimc3  24477  lhop1  24611  ulmcaulem  24982  ulmcau  24983  ulmcn  24987  xrlimcnp  25546  ax5seglem4  26718  axcontlem2  26751  axcontlem4  26753  incistruhgr  26864  nbuhgr  27125  uhgrnbgr0nb  27136  wwlknp  27621  wwlksnred  27670  clwlkclwwlklem2a  27776  vdgn0frgrv2  28074  nmcvcn  28472  htthlem  28694  atcvat3i  30173  sumdmdlem2  30196  ifeqeqx  30297  bnj23  31988  bnj849  32197  prsrcmpltd  32347  cusgr3cyclex  32383  satffunlem2lem1  32651  sotr3  33002  funbreq  33013  nosepssdm  33190  cgrdegen  33465  lineext  33537  btwnconn1lem7  33554  btwnconn1lem14  33561  waj-ax  33762  lukshef-ax2  33763  relowlssretop  34647  finxpreclem6  34680  pibt2  34701  fin2solem  34893  poimirlem2  34909  poimirlem18  34925  poimirlem21  34928  poimirlem26  34933  poimirlem27  34934  poimirlem31  34938  unirep  35003  seqpo  35037  ssbnd  35081  intidl  35322  prnc  35360  prtlem15  36026  lshpkrlem6  36266  atlatmstc  36470  cvrat3  36593  ps-2  36629  2lplnj  36771  paddasslem5  36975  dochkrshp4  38540  rexlimdv3d  39300  isnacs3  39327  pm14.24  40784  rexlim2d  41926  iccpartigtl  43603  icceuelpartlem  43615  prproropf1olem4  43688  rngcinv  44272  rngcinvALTV  44284  ringcinv  44323  ringcinvALTV  44347  lindslinindsimp1  44532  lindslinindsimp2  44538  digexp  44687  aacllem  44922