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

This theorem is referenced by:  rexlimdvv  3221  ralcom2  3288  ssexnelpss  4044  wereu2  5577  oneqmini  6302  suctr  6334  fiunlem  7758  poxp  7940  suppssr  7983  suppssrg  7984  smoel  8162  omabs  8441  omsmo  8448  iiner  8536  fodomr  8864  fisseneq  8963  suplub2  9150  supnub  9151  infglb  9179  infnlb  9181  inf3lem6  9321  cfcoflem  9959  coftr  9960  zorn2lem7  10189  alephreg  10269  inar1  10462  gruen  10499  letr  10999  lbzbi  12605  xrletr  12821  xmullem  12927  supxrun  12979  ssfzoulel  13409  ssfzo12bi  13410  hashbnd  13978  fi1uzind  14139  brfi1indALT  14142  cau3lem  14994  summo  15357  mertenslem2  15525  prodmolem2  15573  alzdvds  15957  nno  16019  nn0seqcvgd  16203  lcmdvds  16241  lcmf  16266  2mulprm  16326  divgcdodd  16343  prmpwdvds  16533  catpropd  17335  pltnle  17971  pltval3  17972  pltletr  17976  tsrlemax  18219  frgpnabllem1  19389  cyggexb  19415  abvn0b  20486  isphld  20771  indistopon  22059  restntr  22241  cnprest  22348  lmss  22357  lmmo  22439  2ndcdisj  22515  txlm  22707  flftg  23055  bndth  24027  iscmet3  24362  bcthlem5  24397  ovolicc2lem4  24589  ellimc3  24948  lhop1  25083  ulmcaulem  25458  ulmcau  25459  ulmcn  25463  xrlimcnp  26023  ax5seglem4  27203  axcontlem2  27236  axcontlem4  27238  incistruhgr  27352  nbuhgr  27613  uhgrnbgr0nb  27624  wwlknp  28109  wwlksnred  28158  clwlkclwwlklem2a  28263  vdgn0frgrv2  28560  nmcvcn  28958  htthlem  29180  atcvat3i  30659  sumdmdlem2  30682  ifeqeqx  30786  bnj23  32597  bnj849  32805  prsrcmpltd  32955  cusgr3cyclex  32998  satffunlem2lem1  33266  onunel  33592  sotr3  33639  funbreq  33650  nosepssdm  33816  cgrdegen  34233  lineext  34305  btwnconn1lem7  34322  btwnconn1lem14  34329  waj-ax  34530  lukshef-ax2  34531  relowlssretop  35461  finxpreclem6  35494  pibt2  35515  fin2solem  35690  poimirlem2  35706  poimirlem18  35722  poimirlem21  35725  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  unirep  35798  seqpo  35832  ssbnd  35873  intidl  36114  prnc  36152  prtlem15  36816  lshpkrlem6  37056  atlatmstc  37260  cvrat3  37383  ps-2  37419  2lplnj  37561  paddasslem5  37765  dochkrshp4  39330  dvdsexpnn0  40262  rexlimdv3d  40421  isnacs3  40448  pm14.24  41939  rexlim2d  43056  iccpartigtl  44763  icceuelpartlem  44775  prproropf1olem4  44846  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  lindslinindsimp1  45686  lindslinindsimp2  45692  digexp  45841  aacllem  46391