Theorem expdimp 451

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  rexlimdvv  3201  ralcom2  3361  ssexnelpss  4110  sotr3  5628  wereu2  5674  oneqmini  6421  suctr  6455  onunel  6474  fiunlem  7944  poxp  8131  suppssr  8199  suppssrg  8200  smoel  8379  omabs  8670  omsmo  8677  iiner  8806  fodomr  9151  fisseneq  9280  suplub2  9484  supnub  9485  infglb  9513  infnlb  9515  inf3lem6  9656  cfcoflem  10295  coftr  10296  zorn2lem7  10525  alephreg  10605  inar1  10798  gruen  10835  letr  11338  lbzbi  12950  xrletr  13169  xmullem  13275  supxrun  13327  ssfzoulel  13758  ssfzo12bi  13759  hashbnd  14327  fi1uzind  14490  brfi1indALT  14493  cau3lem  15333  summo  15695  mertenslem2  15863  prodmolem2  15911  alzdvds  16296  nno  16358  nn0seqcvgd  16540  lcmdvds  16578  lcmf  16603  2mulprm  16663  divgcdodd  16680  prmpwdvds  16872  catpropd  17688  pltnle  18329  pltval3  18330  pltletr  18334  tsrlemax  18577  frgpnabllem1  19832  cyggexb  19858  rngcinv  20574  abvn0b  21256  isphld  21590  indistopon  22934  restntr  23116  cnprest  23223  lmss  23232  lmmo  23314  2ndcdisj  23390  txlm  23582  flftg  23930  bndth  24914  iscmet3  25251  bcthlem5  25286  ovolicc2lem4  25479  ellimc3  25838  lhop1  25977  ulmcaulem  26360  ulmcau  26361  ulmcn  26365  xrlimcnp  26930  nosepssdm  27649  ax5seglem4  28799  axcontlem2  28832  axcontlem4  28834  incistruhgr  28948  nbuhgr  29212  uhgrnbgr0nb  29223  wwlknp  29710  wwlksnred  29759  clwlkclwwlklem2a  29864  vdgn0frgrv2  30161  nmcvcn  30561  htthlem  30783  atcvat3i  32262  sumdmdlem2  32285  ifeqeqx  32390  bnj23  34419  bnj849  34626  prsrcmpltd  34776  cusgr3cyclex  34816  satffunlem2lem1  35084  funbreq  35435  cgrdegen  35670  lineext  35742  btwnconn1lem7  35759  btwnconn1lem14  35766  waj-ax  35968  lukshef-ax2  35969  relowlssretop  36912  finxpreclem6  36945  pibt2  36966  fin2solem  37149  poimirlem2  37165  poimirlem18  37181  poimirlem21  37184  poimirlem26  37189  poimirlem27  37190  poimirlem31  37194  unirep  37257  seqpo  37290  ssbnd  37331  intidl  37572  prnc  37610  eldisjlem19  38351  prtlem15  38416  lshpkrlem6  38656  atlatmstc  38860  cvrat3  38984  ps-2  39020  2lplnj  39162  paddasslem5  39366  dochkrshp4  40931  dvdsexpnn0  41966  rexlimdv3d  42168  isnacs3  42195  cantnfresb  42818  dflim5  42823  onmcl  42825  oaun3lem1  42868  pm14.24  43934  rexlim2d  45076  iccpartigtl  46826  icceuelpartlem  46838  prproropf1olem4  46909  rngcinvALTV  47450  lindslinindsimp1  47637  lindslinindsimp2  47643  digexp  47792  aacllem  48346