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  3188  rexlimdvvva  3190  ralcom2  3343  ssexnelpss  4065  sotr3  5568  wereu2  5616  oneqmini  6365  suctr  6400  onunel  6419  fiunlem  7880  poxp  8064  suppssr  8131  suppssrg  8132  smoel  8286  omabs  8572  omsmo  8579  iiner  8719  fodomr  9047  fisseneq  9153  suplub2  9351  supnub  9352  infglb  9381  infnlb  9383  inf3lem6  9529  cfcoflem  10169  coftr  10170  zorn2lem7  10399  alephreg  10479  inar1  10672  gruen  10709  letr  11213  lbzbi  12840  xrletr  13063  xmullem  13169  supxrun  13221  ssfzoulel  13666  ssfzo12bi  13667  hashbnd  14249  fi1uzind  14420  brfi1indALT  14423  cau3lem  15268  summo  15630  mertenslem2  15798  prodmolem2  15848  alzdvds  16237  nno  16299  nn0seqcvgd  16487  lcmdvds  16525  lcmf  16550  2mulprm  16610  divgcdodd  16627  prmpwdvds  16822  catpropd  17621  pltnle  18248  pltval3  18249  pltletr  18253  tsrlemax  18498  frgpnabllem1  19791  cyggexb  19817  rngcinv  20558  abvn0b  20757  isphld  21597  indistopon  22922  restntr  23103  cnprest  23210  lmss  23219  lmmo  23301  2ndcdisj  23377  txlm  23569  flftg  23917  bndth  24890  iscmet3  25226  bcthlem5  25261  ovolicc2lem4  25454  ellimc3  25813  lhop1  25952  ulmcaulem  26336  ulmcau  26337  ulmcn  26341  xrlimcnp  26911  nosepssdm  27631  ax5seglem4  28917  axcontlem2  28950  axcontlem4  28952  incistruhgr  29064  nbuhgr  29328  uhgrnbgr0nb  29339  wwlknp  29828  wwlksnred  29877  clwlkclwwlklem2a  29985  vdgn0frgrv2  30282  nmcvcn  30682  htthlem  30904  atcvat3i  32383  sumdmdlem2  32406  ifeqeqx  32529  bnj23  34737  bnj849  34944  prsrcmpltd  35100  cusgr3cyclex  35187  satffunlem2lem1  35455  funbreq  35821  cgrdegen  36055  lineext  36127  btwnconn1lem7  36144  btwnconn1lem14  36151  waj-ax  36465  lukshef-ax2  36466  relowlssretop  37414  finxpreclem6  37447  pibt2  37468  fin2solem  37652  poimirlem2  37668  poimirlem18  37684  poimirlem21  37687  poimirlem26  37692  poimirlem27  37693  poimirlem31  37697  unirep  37760  seqpo  37793  ssbnd  37834  intidl  38075  prnc  38113  eldisjlem19  38914  prtlem15  38980  lshpkrlem6  39220  atlatmstc  39424  cvrat3  39547  ps-2  39583  2lplnj  39725  paddasslem5  39929  dochkrshp4  41494  dvdsexpnn0  42433  rexlimdv3d  42781  isnacs3  42808  cantnfresb  43422  dflim5  43427  onmcl  43429  oaun3lem1  43472  pm14.24  44530  traxext  45075  rexlim2d  45730  iccpartigtl  47528  icceuelpartlem  47540  prproropf1olem4  47611  grimedg  48040  pgnbgreunbgrlem3  48223  pgnbgreunbgrlem6  48229  rngcinvALTV  48381  lindslinindsimp1  48563  lindslinindsimp2  48569  digexp  48713  aacllem  49907