Theorem expdimp 453

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  rexlimdvv  3223  ralcom2  3291  ssexnelpss  4049  wereu2  5587  oneqmini  6321  suctr  6353  fiunlem  7793  poxp  7978  suppssr  8021  suppssrg  8022  smoel  8200  omabs  8490  omsmo  8497  iiner  8587  fodomr  8924  fisseneq  9043  suplub2  9229  supnub  9230  infglb  9258  infnlb  9260  inf3lem6  9400  cfcoflem  10037  coftr  10038  zorn2lem7  10267  alephreg  10347  inar1  10540  gruen  10577  letr  11078  lbzbi  12685  xrletr  12901  xmullem  13007  supxrun  13059  ssfzoulel  13490  ssfzo12bi  13491  hashbnd  14059  fi1uzind  14220  brfi1indALT  14223  cau3lem  15075  summo  15438  mertenslem2  15606  prodmolem2  15654  alzdvds  16038  nno  16100  nn0seqcvgd  16284  lcmdvds  16322  lcmf  16347  2mulprm  16407  divgcdodd  16424  prmpwdvds  16614  catpropd  17427  pltnle  18065  pltval3  18066  pltletr  18070  tsrlemax  18313  frgpnabllem1  19483  cyggexb  19509  abvn0b  20582  isphld  20868  indistopon  22160  restntr  22342  cnprest  22449  lmss  22458  lmmo  22540  2ndcdisj  22616  txlm  22808  flftg  23156  bndth  24130  iscmet3  24466  bcthlem5  24501  ovolicc2lem4  24693  ellimc3  25052  lhop1  25187  ulmcaulem  25562  ulmcau  25563  ulmcn  25567  xrlimcnp  26127  ax5seglem4  27309  axcontlem2  27342  axcontlem4  27344  incistruhgr  27458  nbuhgr  27719  uhgrnbgr0nb  27730  wwlknp  28217  wwlksnred  28266  clwlkclwwlklem2a  28371  vdgn0frgrv2  28668  nmcvcn  29066  htthlem  29288  atcvat3i  30767  sumdmdlem2  30790  ifeqeqx  30894  bnj23  32706  bnj849  32914  prsrcmpltd  33064  cusgr3cyclex  33107  satffunlem2lem1  33375  onunel  33698  sotr3  33742  funbreq  33753  nosepssdm  33898  cgrdegen  34315  lineext  34387  btwnconn1lem7  34404  btwnconn1lem14  34411  waj-ax  34612  lukshef-ax2  34613  relowlssretop  35543  finxpreclem6  35576  pibt2  35597  fin2solem  35772  poimirlem2  35788  poimirlem18  35804  poimirlem21  35807  poimirlem26  35812  poimirlem27  35813  poimirlem31  35817  unirep  35880  seqpo  35914  ssbnd  35955  intidl  36196  prnc  36234  prtlem15  36896  lshpkrlem6  37136  atlatmstc  37340  cvrat3  37463  ps-2  37499  2lplnj  37641  paddasslem5  37845  dochkrshp4  39410  dvdsexpnn0  40348  rexlimdv3d  40512  isnacs3  40539  pm14.24  42057  rexlim2d  43173  iccpartigtl  44886  icceuelpartlem  44898  prproropf1olem4  44969  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  ringcinvALTV  45625  lindslinindsimp1  45809  lindslinindsimp2  45815  digexp  45964  aacllem  46516