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  3252  ralcom2  3316  ssexnelpss  4041  wereu2  5516  oneqmini  6210  suctr  6242  fiunlem  7625  poxp  7805  suppssr  7844  smoel  7980  omabs  8257  omsmo  8264  iiner  8352  fodomr  8652  fisseneq  8713  suplub2  8909  supnub  8910  infglb  8938  infnlb  8940  inf3lem6  9080  cfcoflem  9683  coftr  9684  zorn2lem7  9913  alephreg  9993  inar1  10186  gruen  10223  letr  10723  lbzbi  12324  xrletr  12539  xmullem  12645  supxrun  12697  ssfzoulel  13126  ssfzo12bi  13127  hashbnd  13692  fi1uzind  13851  brfi1indALT  13854  cau3lem  14706  summo  15066  mertenslem2  15233  prodmolem2  15281  alzdvds  15662  nno  15723  nn0seqcvgd  15904  lcmdvds  15942  lcmf  15967  2mulprm  16027  divgcdodd  16044  prmpwdvds  16230  catpropd  16971  pltnle  17568  pltval3  17569  pltletr  17573  tsrlemax  17822  frgpnabllem1  18986  cyggexb  19012  abvn0b  20068  isphld  20343  indistopon  21606  restntr  21787  cnprest  21894  lmss  21903  lmmo  21985  2ndcdisj  22061  txlm  22253  flftg  22601  bndth  23563  iscmet3  23897  bcthlem5  23932  ovolicc2lem4  24124  ellimc3  24482  lhop1  24617  ulmcaulem  24989  ulmcau  24990  ulmcn  24994  xrlimcnp  25554  ax5seglem4  26726  axcontlem2  26759  axcontlem4  26761  incistruhgr  26872  nbuhgr  27133  uhgrnbgr0nb  27144  wwlknp  27629  wwlksnred  27678  clwlkclwwlklem2a  27783  vdgn0frgrv2  28080  nmcvcn  28478  htthlem  28700  atcvat3i  30179  sumdmdlem2  30202  ifeqeqx  30309  bnj23  32098  bnj849  32307  prsrcmpltd  32457  cusgr3cyclex  32496  satffunlem2lem1  32764  sotr3  33115  funbreq  33126  nosepssdm  33303  cgrdegen  33578  lineext  33650  btwnconn1lem7  33667  btwnconn1lem14  33674  waj-ax  33875  lukshef-ax2  33876  relowlssretop  34780  finxpreclem6  34813  pibt2  34834  fin2solem  35043  poimirlem2  35059  poimirlem18  35075  poimirlem21  35078  poimirlem26  35083  poimirlem27  35084  poimirlem31  35088  unirep  35151  seqpo  35185  ssbnd  35226  intidl  35467  prnc  35505  prtlem15  36171  lshpkrlem6  36411  atlatmstc  36615  cvrat3  36738  ps-2  36774  2lplnj  36916  paddasslem5  37120  dochkrshp4  38685  rexlimdv3d  39624  isnacs3  39651  pm14.24  41136  rexlim2d  42267  iccpartigtl  43940  icceuelpartlem  43952  prproropf1olem4  44023  rngcinv  44605  rngcinvALTV  44617  ringcinv  44656  ringcinvALTV  44680  lindslinindsimp1  44866  lindslinindsimp2  44872  digexp  45021  aacllem  45329