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  3202  ralcom2  3365  ssexnelpss  4105  sotr3  5617  wereu2  5663  oneqmini  6406  suctr  6440  onunel  6459  fiunlem  7921  poxp  8108  suppssr  8175  suppssrg  8176  smoel  8355  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  11305  lbzbi  12917  xrletr  13134  xmullem  13240  supxrun  13292  ssfzoulel  13723  ssfzo12bi  13724  hashbnd  14293  fi1uzind  14455  brfi1indALT  14458  cau3lem  15298  summo  15660  mertenslem2  15828  prodmolem2  15876  alzdvds  16260  nno  16322  nn0seqcvgd  16504  lcmdvds  16542  lcmf  16567  2mulprm  16627  divgcdodd  16644  prmpwdvds  16836  catpropd  17652  pltnle  18293  pltval3  18294  pltletr  18298  tsrlemax  18541  frgpnabllem1  19783  cyggexb  19809  rngcinv  20523  abvn0b  21204  isphld  21515  indistopon  22826  restntr  23008  cnprest  23115  lmss  23124  lmmo  23206  2ndcdisj  23282  txlm  23474  flftg  23822  bndth  24806  iscmet3  25143  bcthlem5  25178  ovolicc2lem4  25371  ellimc3  25730  lhop1  25869  ulmcaulem  26247  ulmcau  26248  ulmcn  26252  xrlimcnp  26816  nosepssdm  27535  ax5seglem4  28659  axcontlem2  28692  axcontlem4  28694  incistruhgr  28808  nbuhgr  29069  uhgrnbgr0nb  29080  wwlknp  29566  wwlksnred  29615  clwlkclwwlklem2a  29720  vdgn0frgrv2  30017  nmcvcn  30417  htthlem  30639  atcvat3i  32118  sumdmdlem2  32141  ifeqeqx  32243  bnj23  34218  bnj849  34425  prsrcmpltd  34575  cusgr3cyclex  34616  satffunlem2lem1  34884  funbreq  35236  cgrdegen  35471  lineext  35543  btwnconn1lem7  35560  btwnconn1lem14  35567  waj-ax  35789  lukshef-ax2  35790  relowlssretop  36734  finxpreclem6  36767  pibt2  36788  fin2solem  36964  poimirlem2  36980  poimirlem18  36996  poimirlem21  36999  poimirlem26  37004  poimirlem27  37005  poimirlem31  37009  unirep  37072  seqpo  37105  ssbnd  37146  intidl  37387  prnc  37425  eldisjlem19  38170  prtlem15  38235  lshpkrlem6  38475  atlatmstc  38679  cvrat3  38803  ps-2  38839  2lplnj  38981  paddasslem5  39185  dochkrshp4  40750  dvdsexpnn0  41721  rexlimdv3d  41910  isnacs3  41937  cantnfresb  42563  dflim5  42568  onmcl  42570  oaun3lem1  42613  pm14.24  43680  rexlim2d  44826  iccpartigtl  46576  icceuelpartlem  46588  prproropf1olem4  46659  rngcinvALTV  47139  lindslinindsimp1  47326  lindslinindsimp2  47332  digexp  47481  aacllem  48036