Theorem expdimp 456

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  rexlimdvv  3204  ralcom2  3267  ssexnelpss  4014  wereu2  5532  oneqmini  6233  suctr  6265  fiunlem  7680  poxp  7860  suppssr  7903  suppssrg  7904  smoel  8038  omabs  8317  omsmo  8324  iiner  8412  fodomr  8730  fisseneq  8820  suplub2  9010  supnub  9011  infglb  9039  infnlb  9041  inf3lem6  9181  cfcoflem  9784  coftr  9785  zorn2lem7  10014  alephreg  10094  inar1  10287  gruen  10324  letr  10824  lbzbi  12430  xrletr  12646  xmullem  12752  supxrun  12804  ssfzoulel  13234  ssfzo12bi  13235  hashbnd  13800  fi1uzind  13961  brfi1indALT  13964  cau3lem  14816  summo  15179  mertenslem2  15345  prodmolem2  15393  alzdvds  15777  nno  15839  nn0seqcvgd  16023  lcmdvds  16061  lcmf  16086  2mulprm  16146  divgcdodd  16163  prmpwdvds  16352  catpropd  17095  pltnle  17704  pltval3  17705  pltletr  17709  tsrlemax  17958  frgpnabllem1  19124  cyggexb  19150  abvn0b  20206  isphld  20482  indistopon  21764  restntr  21945  cnprest  22052  lmss  22061  lmmo  22143  2ndcdisj  22219  txlm  22411  flftg  22759  bndth  23722  iscmet3  24057  bcthlem5  24092  ovolicc2lem4  24284  ellimc3  24643  lhop1  24778  ulmcaulem  25153  ulmcau  25154  ulmcn  25158  xrlimcnp  25718  ax5seglem4  26890  axcontlem2  26923  axcontlem4  26925  incistruhgr  27036  nbuhgr  27297  uhgrnbgr0nb  27308  wwlknp  27793  wwlksnred  27842  clwlkclwwlklem2a  27947  vdgn0frgrv2  28244  nmcvcn  28642  htthlem  28864  atcvat3i  30343  sumdmdlem2  30366  ifeqeqx  30471  bnj23  32279  bnj849  32488  prsrcmpltd  32638  cusgr3cyclex  32681  satffunlem2lem1  32949  onunel  33275  sotr3  33319  funbreq  33330  nosepssdm  33544  cgrdegen  33961  lineext  34033  btwnconn1lem7  34050  btwnconn1lem14  34057  waj-ax  34258  lukshef-ax2  34259  relowlssretop  35189  finxpreclem6  35222  pibt2  35243  fin2solem  35418  poimirlem2  35434  poimirlem18  35450  poimirlem21  35453  poimirlem26  35458  poimirlem27  35459  poimirlem31  35463  unirep  35526  seqpo  35560  ssbnd  35601  intidl  35842  prnc  35880  prtlem15  36544  lshpkrlem6  36784  atlatmstc  36988  cvrat3  37111  ps-2  37147  2lplnj  37289  paddasslem5  37493  dochkrshp4  39058  dvdsexpnn0  39958  rexlimdv3d  40117  isnacs3  40144  pm14.24  41628  rexlim2d  42748  iccpartigtl  44456  icceuelpartlem  44468  prproropf1olem4  44539  rngcinv  45120  rngcinvALTV  45132  ringcinv  45171  ringcinvALTV  45195  lindslinindsimp1  45379  lindslinindsimp2  45385  digexp  45534  aacllem  46005