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

This theorem is referenced by:  rexlimdvv  3194  rexlimdvvva  3196  ralcom2  3353  ssexnelpss  4082  sotr3  5590  wereu2  5638  oneqmini  6388  suctr  6423  onunel  6442  fiunlem  7923  poxp  8110  suppssr  8177  suppssrg  8178  smoel  8332  omabs  8618  omsmo  8625  iiner  8765  fodomr  9098  fisseneq  9211  suplub2  9419  supnub  9420  infglb  9449  infnlb  9451  inf3lem6  9593  cfcoflem  10232  coftr  10233  zorn2lem7  10462  alephreg  10542  inar1  10735  gruen  10772  letr  11275  lbzbi  12902  xrletr  13125  xmullem  13231  supxrun  13283  ssfzoulel  13728  ssfzo12bi  13729  hashbnd  14308  fi1uzind  14479  brfi1indALT  14482  cau3lem  15328  summo  15690  mertenslem2  15858  prodmolem2  15908  alzdvds  16297  nno  16359  nn0seqcvgd  16547  lcmdvds  16585  lcmf  16610  2mulprm  16670  divgcdodd  16687  prmpwdvds  16882  catpropd  17677  pltnle  18304  pltval3  18305  pltletr  18309  tsrlemax  18552  frgpnabllem1  19810  cyggexb  19836  rngcinv  20553  abvn0b  20752  isphld  21570  indistopon  22895  restntr  23076  cnprest  23183  lmss  23192  lmmo  23274  2ndcdisj  23350  txlm  23542  flftg  23890  bndth  24864  iscmet3  25200  bcthlem5  25235  ovolicc2lem4  25428  ellimc3  25787  lhop1  25926  ulmcaulem  26310  ulmcau  26311  ulmcn  26315  xrlimcnp  26885  nosepssdm  27605  ax5seglem4  28866  axcontlem2  28899  axcontlem4  28901  incistruhgr  29013  nbuhgr  29277  uhgrnbgr0nb  29288  wwlknp  29780  wwlksnred  29829  clwlkclwwlklem2a  29934  vdgn0frgrv2  30231  nmcvcn  30631  htthlem  30853  atcvat3i  32332  sumdmdlem2  32355  ifeqeqx  32478  bnj23  34715  bnj849  34922  prsrcmpltd  35078  cusgr3cyclex  35130  satffunlem2lem1  35398  funbreq  35764  cgrdegen  35999  lineext  36071  btwnconn1lem7  36088  btwnconn1lem14  36095  waj-ax  36409  lukshef-ax2  36410  relowlssretop  37358  finxpreclem6  37391  pibt2  37412  fin2solem  37607  poimirlem2  37623  poimirlem18  37639  poimirlem21  37642  poimirlem26  37647  poimirlem27  37648  poimirlem31  37652  unirep  37715  seqpo  37748  ssbnd  37789  intidl  38030  prnc  38068  eldisjlem19  38809  prtlem15  38875  lshpkrlem6  39115  atlatmstc  39319  cvrat3  39443  ps-2  39479  2lplnj  39621  paddasslem5  39825  dochkrshp4  41390  dvdsexpnn0  42329  rexlimdv3d  42678  isnacs3  42705  cantnfresb  43320  dflim5  43325  onmcl  43327  oaun3lem1  43370  pm14.24  44428  traxext  44974  rexlim2d  45630  iccpartigtl  47428  icceuelpartlem  47440  prproropf1olem4  47511  grimedg  47939  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  rngcinvALTV  48268  lindslinindsimp1  48450  lindslinindsimp2  48456  digexp  48600  aacllem  49794